Sun Mar 14 11:36:26 CET 2010

Encoding `find' in types?

I think the big question is really: should the environemnt
representation be tagless or not?  Is it ok to simply cons elements of
a shared sum type onto a list and read them out later, or should the
binding environment be in the type?

Let's try the tagless approach.

Suppose I have types R0, R1 that statically encode certain registers.
Suppose I have a current enviroment (R1,(R0, ())).  Suppose the type
of the current context is R0.  Is it possible to have a single `read'
operation that fishes out the R0 from the whole type environment?
I.e. can you encode `find' in types?

Ok. I got up to this:

class Ref e r where ref :: e -> r

instance Ref (r,e') r  where ref (x,y) = x
instance Ref e' r' => Ref (r,e') r' where ref (x,y) = ref y

However, the latter doesn't work as it needs the extra constraint r /=
r'.  How to add this constraint?  Apperently[1] this type constraint
should work:

                  TypeEq t1 t2 False

There's a package HList[2] that does most of the magic.  However, I'd
like to reconstruct it from the basics first.  How to add that type

Anyways, -XOverlappingInstances solves the problem, but I read
somewhere that equality is not always well-defined.  I don't
understand.  Let's stick to this solution until it becomes a problem.
It seems that HList[2] avoids overlapping instances.

[1] http://www.haskell.org/pipermail/haskell-cafe/2006-April/015372.html
[2] http://homepages.cwi.nl/~ralf/HList/