Sat Jul 23 21:27:22 CEST 2011

GADTs for typed assembly language

In [1] GADTs are used for representing a typed assembly language.  The
reason seems to be that it's not possible to construct something of
the following type using just data types:

   Term a -> Term b

which was necessary for type conversion functions:

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

[1] http://okmij.org/ftp/tagless-final/Incope.hs