问题描述
使用 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等相关库。