Implementing untyped PCF in typed PCF

For TLCA 2003 I wrote a paper showing that any well-behaving untyped PCF term can be equivalently expressed by a well-typed term.
This is based on the idea of implementing untyped PCF within typed PCF.

To elaborate: in order to interpret an untyped PCF term at a higher type we have to be able to pass typed values as arguments to that term, the implementation effectively evaluates an untyped open a term in a typed environment. To allow to integrate the typed world with the least hassle possible we lift typed values to those types that are also used as approximants in the D_∞ model.
The Haskell implementation consists of three files:

PCF.hs (the main implementation),
Exp.hs (abstract syntax for PCF plus some related auxiliary functions like substitution)
LUB.hs (a module to compute upper bounds for types, also containing stuff on retractions)

Notice that the code requires GHC (because Hugs binds variables in class instances differently), and also the "Glasgow extensions", i.e. this should be run using

ghci -fglasgow-exts

One proviso: the interpret function is overloaded, but resolving that overloading within the GHC interpreter seems to have the potential to make the interpreter fall over (a bug in GHC) - this does not happen when the overload resolution is done in a file. This is the reason why PCF.hs contains several examples of resolved instances of interpret.

Stefan Kahrs