小编fly*_*eep的帖子

我想编写一个函数，用 GADT 样式定义的数据结构将正则 lambda 表达式转换为 DeBrujin 样式。

{-# Language GADTs, StandaloneDeriving,ScopedTypeVariables #-}

module DeBrujin where

import Debug.Trace
import Data.List as L

data Apply
data Abstract
data Variable

data LambdaTerm a where
  Var :: String -> LambdaTerm Variable
  Abs :: String -> LambdaTerm a -> LambdaTerm Abstract
  App :: LambdaTerm Abstract -> LambdaTerm a -> LambdaTerm Apply

instance Show (LambdaTerm a) where
  show (Var v) = v
  show (Abs s t) = "?" ++ s ++ "." ++ show t
  show …