Re: Type classes and type equality

Neil Mitchell wrote:
I'm looking for a type class which checks whether two types are the same or not.
This problem is more complex than appears. It has been solved, however. IncoherentInstances are not required, as IncoherentInstances are generally unsafe. For the full discussion of various solutions, please see Section 9 and Appendix D of the HList paper: http://homepages.cwi.nl/~ralf/HList/paper.pdf The HList code is available http://darcs.haskell.org/HList/ It includes the examples from the paper.

Hi Oleg,
I'm looking for a type class which checks whether two types are the same or not.
For the full discussion of various solutions, please see Section 9 and Appendix D of the HList paper: http://homepages.cwi.nl/~ralf/HList/paper.pdf
Thanks for pointing that out. As far as I can see, this requires a new instance declaration for every type? In this sense, it would require as many Typeable declarations, but have the downside that it isn't build into any compiler. I was really hoping for something that requires less work on behalf of the user. Thanks Neil

Thanks for pointing that out. As far as I can see, this requires a new instance declaration for every type?
I guess it depends on how many extensions one may wish to enable. At the very least we need multi-parameter type classes with functional dependencies (because that's what TypeEq is in any case). - If we permit no other extension, we need N^2 instances to compare N classes for equality (basically, for each type we should say how it compares to the others). This is not practical except in very limited circumstances. - If we permit undecidable instances, one may assign numerals to types. This gives us total order and hence comparison on types. In this approach, we only need N instances to cover N types. This is still better than Typeable because the equality is decided and can be acted upon at compile time. - If we permit overlapping instances extension, then a few lines of code decide equality for all existing and future types: class TypeEq x y b | x y -> b instance TypeEq x x HTrue instance TypeCast HFalse b => TypeEq x y b Please see http://www.haskell.org/pipermail/haskell-cafe/2006-November/019705.html for some less conventional application, with the complete code.
I was really hoping for something that requires less work on behalf of the user.
The latter approach may be suitable then. It requires no work on behalf of the user at all: the type comparison is universal. http://darcs.haskell.org/HList There is also an issue of ground vs unground types. All the approaches above can decide equality for sufficiently grounded types. That is, two types can be decided equal only if they are ground. The disequality may be decided for partially ground types. If the types are non-ground, the TypeEq constraint flows up, to be resolved when the types are sufficiently instantiated. It is possible to decide equality of non-ground types and even naked type variables. That is a separate discussion.

Hi
I guess it depends on how many extensions one may wish to enable. At the very least we need multi-parameter type classes with functional dependencies (because that's what TypeEq is in any case).
- If we permit no other extension, we need N^2 instances to compare N classes for equality (basically, for each type we should say how it compares to the others). This is not practical except in very limited circumstances.
- If we permit undecidable instances, one may assign numerals to types. This gives us total order and hence comparison on types. In this approach, we only need N instances to cover N types. This is still better than Typeable because the equality is decided and can be acted upon at compile time.
In my particular case whether I act at compile time or run time is unimportant, but obviously this is an important advantage in general. Unfortunately a cost of one instance per type is still higher than I'd like to pay :-)
- If we permit overlapping instances extension, then a few lines of code decide equality for all existing and future types:
class TypeEq x y b | x y -> b instance TypeEq x x HTrue instance TypeCast HFalse b => TypeEq x y b
This is exactly what I was after, but it doesn't seem to work in Hugs - even with overlapping instances and unsafe overlapping instances turned on. *** This instance : TypeEq a b c *** Conflicts with : TypeEq a a HTrue *** For class : TypeEq a b c *** Under dependency : a b -> c Is there any way to modify this to allow it to work under Hugs as well? Thanks very much for your help, Neil

On Wed, Apr 18, 2007 at 01:47:04AM +0100, Neil Mitchell wrote:
- If we permit undecidable instances, one may assign numerals to types. This gives us total order and hence comparison on types. In this approach, we only need N instances to cover N types. This is still better than Typeable because the equality is decided and can be acted upon at compile time.
In my particular case whether I act at compile time or run time is unimportant, but obviously this is an important advantage in general. Unfortunately a cost of one instance per type is still higher than I'd like to pay :-)
Now, it requires one line of code: {-# OPTIONS_DERIVE --derive=TTypeable #-} Stefan

- If we permit overlapping instances extension, then a few lines of code decide equality for all existing and future types:
class TypeEq x y b | x y -> b instance TypeEq x x HTrue instance TypeCast HFalse b => TypeEq x y b
This is exactly what I was after, but it doesn't seem to work in Hugs - even with overlapping instances and unsafe overlapping instances turned on.
Hugs is indeed quite problematic; back in 2004 we essentially gave up on Hugs for anything moderately advanced, especially after Ralf found an example which typechecks only if constraints are specified in a particular order. If we permute the constraints (I think, it was in the instance declaration), Hugs complaints. Clearly the order of constraints should not matter. It has been my experience that the code requiring undecidable instances on GHC might not work on Hugs, failing with sometimes bizarre error messages.
participants (3)
-
Neil Mitchell
-
oleg@pobox.com
-
Stefan O'Rear