Martin Hofmann asked:

Is there a Haskell implementation of the paper "Typing Dynamic Typing" by Baars and Swierstra

There is a different implementation but in the same spirit http://okmij.org/ftp/tagless-final/IncopeTypecheck.hs http://okmij.org/ftp/Computation/tagless-typed.html#tc-final The first difference between IncopeTypecheck and Baars and Swierstra's one is in the type representation and safe coercions. IncopeTypecheck uses Typeable, and so it needs to define reflection from a type rep to a value of that type. The projection function of Typeable requires a value of a specific type rather than a typerep. The main difference is treating environments and weakening. Baars and Swierstra treat an Identifier, at compile time, as a projection function \env->t. Here env is the run-time env represented as a nested tuple. `Closing the Stage' paper relies on the same idea. To be able to collect those projection functions into a regular list, they wrap them into a Dynamic. IncopeTypecheck, in contrast, represents compile-time variables as functions \x->x, which are weakened as they are embedded into a reacher environment. The functions are wrapped into Dynamic, as this is the result of typechecking. The type environment Gamma in IncopeTypecheck contains only TypeRep but no Dynamics! Here a few examples to illustrate the difference between Baars and Swierstra and IncopeTypecheck: Source expression: Add (Int 2) (Int 3) Baars and Swierstra: \env -> (\_ -> 2) env + (_ -> 3) env IncopeTypecheck: add (int 1) (int 2) Source expression: (Lam "x" Int (x + (Int 1))) Baars and Swierstra: \env -> \x -> (\env -> (\(x,_) ->x) env + (\_ -> 1) env) (x,env) IncopeTypecheck: \x -> (\x -> x) x `add` (\_ -> int 1) x (of course, in IncopeTypecheck, instead of (\x -> ...) there should be lam (\x -> ...) and instead of meta-language application there should be app. I drop them for clarity). For deeply nested functions, IncopeTypecheck probably has to do more redices as it repeatedly applies coercions. Since the environment is known, I could have built the weakening in one step rather than as a sequence of weakening into a progressively richer environment. Each step into this sequence includes an administrative redex. The sequential weakening was easier to implement though.