[Haskell-cafe] Re: in-equality type constraint?

[Paul L]

Thanks a lot for the explanation. Do you think supporting type
inequality test in type families would require UndecidableInstances?
For the reason that wren ng thornton mentioned?

On Sat, Jul 17, 2010 at 4:56 AM,  <oleg at okmij.org> wrote:
>
> Ryan Ingram wrote:
>> But it doesn't generalize; you need to create a witness of inequality
>> for every pair of types you care about.
>
> One can do better, avoiding the quadratic explosion. One merely needs
> to establish a map from a type to a suitable, comparable
> representation -- for example, to a type level list of type level
> numerals. Comparing types for equality, inequality and even order is a
> simple matter of comparing their representations. The fact that types
> become totally ordered lets us even implement type-level maps:
> Data.Map on types. (We may need a Type.* module hierarchy.)
>
>        That idea was described in the HList paper
>        http://homepages.cwi.nl/~ralf/HList/paper.pdf
> Section 9. The code is still available,
>        http://code.haskell.org/HList/examples/TTypeable.hs
> see also TypeEqExplosive.hs, TypeEqTTypeable.hs.
>
>
>> But given the use of UndecidableInstances and OverlappingInstances, I
>> was hoping that type families could come a little cleaner.
>
> Normally if the use of functional dependencies requires
> UndecidableInstances, type families would ask for them too. As to
> OverlappingInstances -- that is the key to generic inequality, isn't
> it?
>
> Given the set of pairs of types, the set of the elements representing
> non-equal types is the complement of the set of elements representing
> equal types (by equal I mean identical). Overlapping instances is the
> way to express set complementation. The most general instance is
> chosen when none of the more specific apply. The set of types chosen
> by that general instance is the complement for the set of types chosen
> by the specific instances.
>
>> Does "TypeEq a c HFalse" imply proof of inequality, or unprovability
>> of equality?
>
> We are all constructivists here... If 'a' and 'c' are type variables,
> (TypeEq a c HFalse) is the constraint -- proof obligation if you will
> -- making sure the variables will never be instantiated to identical
> types. Strictly speaking, the constraint is discharged if 'a' and 'c'
> are two ground, and syntactically distinct (non-identical) types. In
> reality, I think GHC is able to discharge the constraint if 'a' and
> 'c' are grounded ``sufficiently enough'' for the difference to become
> apparent (e.g., the head constructors are different).
>



-- 
Regards,
Paul Liu

Yale Haskell Group
http://www.haskell.org/yale