haskell - 无类型 lambda 演算的冒险

Question

我们偶尔会有人询问如何在 Haskell 中实现无类型 lambda 演算。 [当然，我现在找不到任何这些问题，但我确定我已经看到了!] 只是为了咯咯笑，我想我会花一些时间玩这个。

做类似的事情很简单

i = \ x -> x
k = \ x y -> x
s = \ f g x -> (f x) (g x)

这完美地工作。但是，一旦您尝试做类似的事情

s i i

类型检查器正确地提示无限类型。基本上，无类型 lambda 演算中的所有内容都是一个函数——这本质上意味着所有函数都有无限数量。但是 Haskell 只允许有限元的函数。 (因为，真的，你为什么想要无限的数量？)

好吧，事实证明我们可以轻松地避开这个限制:

data Term = T (Term -> Term)

T f ! x = f x

i = T $ \ x -> x
k = T $ \ x -> T $ \ y -> x
s = T $ \ f -> T $ \ g -> T $ \ x -> (f ! x) ! (g ! x)

这完美地工作，并允许构造和执行任意 lambda 表达式。例如，我们可以轻松构建一个函数来将 Int变成教堂数字:

zero = k ! i
succ = s ! (s ! (k ! s) ! k)

encode 0 = zero
encode n = succ ! (encode $ n-1)

同样，这非常有效。

现在写一个解码函数。

……是的，祝你好运!问题是，我们可以创建任意的 lambda 项，但我们不能以任何方式检查它们。所以我们需要添加一些方法来做到这一点。

到目前为止，我想出的最好的主意是:

data Term x = F (Term x -> Term x) | R (Term x -> x)

F f ! x =            f x
R f ! x = R $ \ _ -> f x

out :: Term x -> x
out (R f) = f (error "mu")
out (F _) =   (error "nu")

i = F $ \ x -> x
k = F $ \ x -> F $ \ y -> x
s = F $ \ f -> F $ \ g -> F $ \ x -> (f ! x) ! (g ! x)

我现在可以做类似的事情

decode :: Term Int -> Int
decode ti = out $ ti ! R (\ tx -> 1 + out tx) ! R (\ tx -> 0)

这对教堂 bool 和教堂数字非常有用。

当我开始尝试做任何高级别的事情时，事情开始变得非常糟糕。抛弃了所有类型信息来实现无类型 lambda 演算后，我现在正努力说服类型检查器让我做我想做的事。

这有效:

something = F $ \ x -> F $ \ n -> F $ \ s -> s ! x
nothing   =            F $ \ n -> F $ \ s -> n

encode :: Maybe x -> Term x
encode (Nothing) = nothing
encode (Just  x) = something ! x

这不会:

decode :: Term x -> Maybe (Term x)
decode tmx = out $ tmx ! R (\ tx -> Nothing) ! R (\ tx -> Just tx)

我已经尝试了十几种轻微的变化；他们都没有类型检查。不是我不明白它为什么会失败，而是我想不出任何方法让它成功。 (尤其是 R Just 显然是错误的类型。)

就好像我想要一个函数 forall x y. Term x -> Term y .因为，对于纯粹的无类型术语，这应该始终是可能的。仅涉及 R 的条款那行不通的地方。但我不知道如何在 Haskell 类型系统中表达它。

(例如，尝试将 F 的类型更改为 forall x. Term x -> Term x 。现在 k 的定义类型错误，因为内部 F $ \ y -> x 实际上不能返回任何类型，而只能返回 [now fixed] 类型 x。)

比我聪明的人有更好的主意吗？

Answer 1

好的，我找到了解决方案:

上面的代码有 Term x ，由 R 的结果类型参数化.而不是这样做(并吓坏类型检查器)，构造一些类型 Value它可以代表您想要返回的每种结果类型。现在我们有

data Term = F (Term -> Term) | R (Term -> Value)

将所有可能的结果类型折叠成一个不透明的 Value类型，我们可以做我们的工作。

具体来说，我选择的类型是

data Value = V Int [Term]

所以一个 Value是 Int表示一个 ADT 值构造函数，后跟一个 Term对于该构造函数的每个字段。有了这个定义，我们终于可以做到了

decode :: Term -> Maybe Term
decode tmx =
  case tmx ! R (\ _ -> V 0 []) ! R (\ tx -> V 1 [tx]) of
    V 0 []   -> Nothing
    V 1 [tx] -> Just tx
    _        -> error "not a Maybe"

同样，您可以像这样对列表进行编码和解码:

null =                        F $ \ n -> F $ \ c -> n
cons = F $ \ x -> n $ \ xs -> F $ \ n -> F $ \ c -> c ! x ! xs

encode :: [Term] -> Term
encode (  []) = null
encode (x:xs) = cons ! x ! encode xs

decode :: Term -> [Term]
decode txs =
  case out $ txs ! R (\ txs -> V 0 []) ! F (\ tx -> R $ \ txs -> V 1 [tx, txs]) of
    V 0 []        -> []
    V 1 [tx, txs] -> tx : decode txs
    _             -> error "not a list"

当然，您必须猜测您需要应用哪些解码功能。但这就是你的无类型 lambda 演算!