使用递归类型在Haskell中编码动态类型的lambda演算

Question

我正在阅读皮尔斯的类型和编程语言一书,在关于递归类型的章节中,他提到它们可以用于用类型语言编码动态lambda演算.作为练习,我正在尝试在Haskell中编写该编码,但我无法通过typechecker:

{-# 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数据类型的原始定义.

Answer 1

这不起作用的原因是因为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