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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
