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

Question

使用 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)

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

Answer 2

如果您想以某种看起来接近任意 lambda 表达式的形式对其进行编码，我怀疑它将需要一些类型级编程来跟踪当前的 lambda 深度。如果在编译时不知道这些术语的类型，这将使​​得组合术语变得困难。

但是，如果您不介意看起来完全不同的等价物，众所周知，SKI 组合子相当于 lambda 演算。而且由于 SKI 根本不提供显式 lambda 或变量引用，因此无法对非封闭项进行编码。