Sat Jul 23 19:32:29 CEST 2011

Type conversions

How to do these:

  -- Type conversions
  i2f   :: repr Tint   -> repr Tfloat
  f2i   :: repr Tfloat -> repr Tint

Trouble seems to be that 2 types don't fit well in (Term a) or (Eval
a) when they are mixed.  How to work around that?

For Eval it seems straightforward:

  i2f = Efloat . fromInteger . eInt
  f2i = Eint . floor . eFloat
For Term I don't see it.  

i2f :: Term Tfloat -> Term Tint
f2i :: Term Tint -> Term Tfloat

Due to the recursive relationship, this doesn't seem to be possible
because you can't graft both term types together.

Should this become (Term i f) ?

I need to look at the cheat sheet[3].  This makes it clear that repr
parameter doesn't need to encode the float/integer types: the
parameter already does.  So what with casts?

The code in [3] either interprets, or compiles to GADT.  The MetaOCaml
code doesn't need that.  Is the code type in MetaOCaml somehow
special, i.e. GADT-like?

So, problem:

  Interpretation of i2f and f2i is not a problem: it is trivial to
  lift :: Double -> Integer to :: Eval Double -> Eval Integer.

  However, using simple recursive types it seems impossible to
  construct something with type :: Term Double -> Term Integer.

But, is this really a problem?  If I use the same approach as in
MetaOCaml - to generate code and never post-process it - then it might
be simpler to skip this step and dump out a textual representation
straight from the syntax class.

[1] http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf
[2] http://www.cs.rutgers.edu/~ccshan/tagless/talk.pdf
[3] http://okmij.org/ftp/tagless-final/Incope.hs