使用递归类型在Haskell中键入lambda微积分
我正在阅读Pierce的类型和编程语言书籍，在关于递归类型的章节中，他提到可以用类型化语言编码动态lambda演算。 作为练习，我试图在Haskell中编写该编码，但我无法通过类型检查器：
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
data D = D (forall x . x -> x )
lam :: (D -> D) -> D
--lam f = D f
lam = undefined
ap :: D -> D -> D
ap (D f) x = f x
--Some examples:
myConst :: D
myConst = lam (x -> lam (y -> x))
flippedAp :: D
flippedAp = lam (x -> lam (f -> ap f x))
现在，这段代码给了我下面的错误信息（我真的不明白）：
dyn.hs:6:11:
Couldn't match type `x' with `D'
`x' is a rigid type variable bound by
a type expected by the context: x -> x at dyn.hs:6:9
Expected type: x -> x
Actual type: D -> D
In the first argument of `D', namely `f'
In the expression: D f
In an equation for `lam': lam f = D f
将lam的定义更改为undefined（注释掉的行）可以编译代码，所以我怀疑我所做的任何错误都是在lam的定义或D数据类型的原始定义中。
这不起作用的原因是因为f :: D -> D D想要一个可以接受任何类型x并返回x 。 这相当于
d :: forall a. a -> a
正如你所看到的，唯一的理智的实现是id 。 尝试
data D = D (D -> D)
...
unit = D id
也许为了更好的印刷：
data D = DFunc (D -> D) | DNumber Int
问题是你的f类型是D -> D （根据你对lam的类型签名），但是D构造函数需要一个类型为forall x . x -> x的参数forall x . x -> x forall x . x -> x 。 这些不是同一类型，所以编译器会抱怨