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

[oleg at okmij.org]

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).