Sat Jul 23 16:29:38 CEST 2011

Typed syntax

I think I'm running into the limitation that is the central idea of
[1].  It is possible to embed a typed language into Haskell, OCaml
without fancy types if a "final" representation is used (generic
functions in Haskell's type classes or OCaml's modules) instead of a
"intial" one (straight up data types).

I'm using the coalgebraic representation, but I'm trying now to work
around some type limitations that hint at the impossibility of being
able to pull that off.

What I don't understand is how this is seemingly sidestepped in

I'm confused.. I think I'm missing one layer of abstraction: my
representation of code (Expr, TExpr) should be final, not initial.

Is it possible to glue that to ordinary Num classes and my sharing

How far am I getting off-track here? :)

[1] http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf