0

我正在阅读 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 数据类型的原始定义中。

4

2 回答 2

5

这不起作用的原因是因为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
于 2013-09-21T03:47:14.643 回答
2

问题是你f有类型D -> D（根据你的类型签名lam），但D构造函数需要一个类型的参数forall x . x -> x。这些不是同一类型，因此编译器会抱怨

于 2013-09-21T03:46:44.263 回答