8

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

4

3 回答 3

7

您可以使用 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
于 2021-05-29T09:20:00.787 回答
4

当然，这甚至被实现为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 级别的数量。

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

这种方法适用于普通的 Haskell 98（即没有 GADT），尽管添加一些花哨的类型有好处，例如我经常将它们用于类型化 AST 和静态类型化类型检查器。Ed Kmett 很好地概述了bound哈斯克尔学院的设计。这个空间中有相关的库，例如unbound和unbound-generics。

于 2021-05-29T19:09:10.303 回答
4

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

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

于 2021-05-29T06:48:20.753 回答