[Haskell-cafe] Typing Dynamic Typing [Was: Dynamically typing TH.Exp at runtime]

oleg at okmij.org oleg at okmij.org
Fri Mar 13 00:33:09 EDT 2009

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


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)
	\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.

More information about the Haskell-Cafe mailing list