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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
