Encoding the dynamicaly-typed lambda calculus in Haskell using recursive types

Question

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.

Daniel Gratzer Daniel Gratzer · Accepted Answer · 2013-09-21T03:47:14

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

Encoding the dynamicaly-typed lambda calculus in Haskell using recursive types

2 Answers