CODEWITHSUNDEEP
haskelltypesfunctional-programminglambda-calculus
hugomg
hugomg

Reputation: 69964

Encoding the dynamicaly-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.

Upvotes: 0

Views: 249

Answers (2)

daniel gratzer
daniel gratzer

Reputation: 53901

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

Upvotes: 5

Gabriella Gonzalez
Gabriella Gonzalez

Reputation: 35099

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. Those are not the same type, so the compiler complains

Upvotes: 2

Related Questions