我正在阅读 Pierce 的 Types and Programming Languages 书,在关于递归类型的章节中,他提到它们可用于在类型化语言中编码动态 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
为未定义(注释掉的行)可以编译代码,所以我怀疑我做错了什么要么是在 lam 的定义中,要么是在 D 数据类型的原始定义中。