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

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

使用 De Bruijn 表示法，可以将 lambda 项定义为：

fgets()

或者使用通常的符号， string.h

这两种数据类型允许构造封闭项和包含自由变量的项。

是否可以定义仅允许构造封闭项的数据类型。即只有以下条款： \x.x，\x。 x x,\x.\y. xy,\x.\y.是， \x.\y.\z.z(x y)

解决方法

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

,

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

但是，如果您不介意看起来完全不同的等价物，那么众所周知，SKI combinators are equivalent to lambda calculus。而且由于 SKI 根本不提供显式 lambda 或变量引用，因此无法对非封闭项进行编码。

,

当然，这甚至在 bound 中作为库实现，这是使用（多态）递归数据类型的 De Bruijn 索引表示的概括：

data Var bound free
  = Bound bound
  | Free free

newtype Scope bound term a
  = Scope { runScope :: term (Var bound (term a)) }

data Term var
  = Var var
  | App (Term var) (Term var)
  | Lam (Scope () Term var)
  -- == Lam (Term (Var () (Term var)))

术语的类型由这些术语中的变量类型索引，包括绑定的和自由的。在 lambda 项中定义新的嵌套作用域时，我们更改了该类型：对于绑定变量，我们只是添加了另一层嵌套，这里用 () 注释以给出简单的 De Bruijn 索引；对于自由变量，我们只是传递类型，而且还添加了一个带有 Term 的嵌套级别。类型级别的嵌套反映了索引可能引用的 De Bruijn 级别的数量。

现在 Term Void 是没有自由变量的项的类型；它可能仍然有绑定变量，因为递归是多态的：Lam (Scope (Var (Bound ()))) :: Term Void 表示 (λx.x)。

这个方法在普通的 Haskell 98（即没有 GADTs）中工作，尽管添加一些花哨的类型有优势，例如我经常将它们用于类型化的 AST 和静态类型的类型检查器。 Ed Kmett 在 Haskell 学院给了一个很好的 overview of the design of bound。这个空间有unbound和unbound-generics等相关库。