typed lambda calculus in Haskell using recursive types
I'm reading Pierce's Types and Programming Languages book and in the chapter about recursive types he mentions that they can be used to encode the dynamic lambda calculus in a typed language. As an exercise, I'm trying to write that encoding in Haskell but I can't get it to pass the 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))
Right now, this code gives me the following error message (that I don't really understand):
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
Changing the definition of lam to undefined (the commented-out line) gets the code to compile so I suspect that whatever I did wrong is either on lam's definition or in the original definition for the D datatype.
The reason this doesn't work is because f :: D -> D . D wants a function which can take in any type x and return x . This is equivalent to
d :: forall a. a -> a
As you can see, the only sane implementation for this is id . Try
data D = D (D -> D)
...
unit = D id
Perhaps for better printing:
data D = DFunc (D -> D) | DNumber Int
The issue is that your f has type D -> D (according to your type signature for lam ), but the D constructor expects an argument of type forall x . x -> x forall x . x -> x . Those are not the same type, so the compiler complains
上一篇: 哈斯克尔杯文件的语法