首页 文章

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

提问于
浏览 次
0

我正在阅读皮尔斯的类型和编程语言一书，在关于递归类型的章节中，他提到它们可以用于用类型语言编码动态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数据类型的原始定义 .

haskell types functional-programming lambda-calculus

2 回答

  • 2

    这不起作用的原因是因为 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
    回复于
  • 5

    问题是 f 的类型为 D -> D （根据 lam 的类型签名），但 D 构造函数需要 forall x . x -> x 类型的参数 . 那些不是同一类型，所以编译器抱怨

    回复于

相关问题