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 this type constraint
TypeEq t1 t2 False
There's a package HList 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 avoids overlapping instances.