无类型化λ微积分历险记

Question

我们偶尔会有人问关于在Haskell中实现无类型lambda演算的问题。[当然，我现在找不到这些问题中的任何一个，但我肯定我已经看到了！]只是为了傻笑，我想我应该花点时间玩这个。

做一些像这样的事情已经足够微不足道了

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

s i i

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)

同样，这是完美的。

现在写一个解码函数。

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)

这是有效的：

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明显是错误的。）

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

Answer 1

好吧，我找到了解决办法：

上面的代码有项X，由R的结果类型参数化。与其这样做（并使类型检查器崩溃），不如构造一些类型值，它可以表示您希望返回的每个结果类型。现在我们有

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

将所有可能的结果类型折叠成一个不透明的value类型后，我们就可以完成工作了。

data Value = V Int [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"

当然，您必须猜测需要应用哪个解码函数。但这是给你的非类型化λ微积分！