是否可以用Haskell或任何其他语言编写一个或多个仅表示封闭项的数据结构？
使用 De Bruijn 表示法，可以将 lambda 项定义为：
data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm
或者使用通常的符号，
data Term = Var String | Lam String Term | App Term Term
这两种数据类型允许构造封闭项和包含自由变量的项。
是否可以定义仅允许构造封闭项的数据类型。即只有诸如：xx、x 之类的术语。xx, x.y. xy, x.y. y, x.y.zz(xy)
回答
您可以使用 GADT 强制自由变量列表为空。自由变量可以保存在类型级列表中。下面，我选择使用 De Bruijn 指数来表示变量。
我们首先定义如何附加两个类型级别列表：
{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, TypeOperators,
GADTs, ScopedTypeVariables, TypeApplications #-}
{-# OPTIONS -Wall #-}
import GHC.TypeLits
import Data.Proxy
-- Type level lists append
type family (xs :: [Nat]) ++ (ys :: [Nat]) :: [Nat] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
然后我们计算 t给定那些的自由变量t。
-- Adjust Debuijn indices under a lambda:
-- remove zeros, decrement positives
type family Lambda (xs :: [Nat]) where
Lambda '[] = '[]
Lambda (0 ': xs) = Lambda xs
Lambda (x ': xs) = x-1 ': Lambda xs
最后是我们的 GADT：
-- "BTerm free" represents a lambda term with free variables "free"
data BTerm (free :: [Nat]) where
BVar :: KnownNat n => BTerm '[n]
BLam :: BTerm free -> BTerm (Lambda free)
BApp :: BTerm free1 -> BTerm free2 -> BTerm (free1 ++ free2)
封闭项的类型现在很容易定义：
-- Closed terms have no free variables
type Closed = BTerm '[]
我们完了。让我们写一些测试。我们从一个Show实例开始，以便能够实际打印条款。
showBVar :: forall n. KnownNat n => BTerm '[n] -> String
showBVar _ = "var" ++ show (natVal (Proxy @n))
instance Show (BTerm free) where
show t@BVar = showBVar t
show (BLam t) = " " ++ show t
show (BApp t1 t2) = "(" ++ show t1 ++ ")(" ++ show t2 ++ ")"
这里有几个测试：
-- x. y. z. z (x y)
-- Output: (var0)((var2)(var1))
test1 :: Closed
test1 = BLam (BLam (BLam (BApp z (BApp x y))))
where
z = BVar @0
y = BVar @1
x = BVar @2
-- x. y. x y (z. z (x y))
-- Output: ((var1)(var0))( (var0)((var2)(var1)))
test2 :: Closed
test2 = BLam (BLam (BApp (BApp x' y') (BLam (BApp z (BApp x y)))))
where
z = BVar @0
y = BVar @1
x = BVar @2
y' = BVar @0
x' = BVar @1
THE END
二维码