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

[oleg at okmij.org]

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.