On 22/06/2011 17:57, Simon Peyton-Jones wrote:
I have long advertised a plan to allow so-called superclass equalities. I've just pushed patches to implement them. So now you can write
class (F a ~ b) => C a b where { ... }
That is fantastic. I have a question about this feature as compared to the two methods used to define the TypeCast superclass equality constraint in HList. Can (~) replace all uses of TypeCast? If not, then can (~) help define TypeCast in a better way? The two existing ways are a bit fragile. I will put the TypeCast definitions below so readers of this question need not go digging. I just refreshed my understanding of TypeCast by re-reading appendix D of the extended technical report for HList at [1,2]. The class TypeCast should only have instances when x and y are unified:
class TypeCast x y | x -> y, y -> x where typeCast :: x -> y
The first definition for TypeCast is simply
instance TypeCast x x where typeCast = id
But this was fragile since the class and instance have to be kept apart and the instance has be imported carefully. Quoting [2]:
To keep the compiler from applying the type simplification rule too early, we should prevent the early inference of the rule from the instance of TypeCast in the first place. For example, we may keep the compiler from seeing the instance TypeCast x x until the very end. That is, we place that instance in a separate module and import it at a higher level in the module hierarchy than all clients of the class TypeCast.
The second definition of TypeCast can be included normally but is quite curious looking:
class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x
The HList authors follow this definition in [2] with:
While this code works in GHC and is logically sound, we have to admit that we turned the drawbacks of the type-checker to our advantage. This leaves a sour after-taste. We would have preferred to rely on a sound semantic theory of overloading rather than on playing games with the type-checker. Hopefully, the results of the foundational work by Sulzmann and others [32, 23] will eventually be implemented in all Haskell compilers.
[1] Page: http://homepages.cwi.nl/~ralf/HList/ [2] Pdf: http://homepages.cwi.nl/~ralf/HList/paper.pdf