haskell - 是否可以用 Haskell 或任何其他语言编写一个或多个仅表示封闭术语的数据结构？

Question

使用 De Bruijn 表示法，可以将 lambda 项定义为:data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm或者使用通常的符号，data Term = Var String | Lam String Term | App Term Term这两种数据类型允许构造封闭项和包含自由变量的项。
是否可以定义一个只允许构造封闭项的数据类型。即只有以下条款:
\x.x，\x。 xx,
\x.\y. xy,
\x.\y.是的，
\x.\y.\z.z(x y)

Answer 1

您可以使用 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