TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

I'd like to summarize the relationship between functional dependencies
and type functions, and propose a solution that should get rid of
overlapping instances. The solution does not require messing with
System-FC. In fact, it can be implemented today (although
ungainly). A small bit of GHC support will be appreciated.

I believe that functional dependencies and type functions are not
comparable. There are examples that can't be done (in principle or in
practice) with type functions, and there are examples that cannot be
implemented with functional dependencies.

The example of the latter is
	http://okmij.org/ftp/Computation/extra-polymorphism.html#injectivity

Functional dependencies have the advantage in the following two cases

 1. mutual dependencies:
	class Add x y z | x y -> z, x z -> y, y z -> x

I think this example can be emulated with type functions; the
emulation didn't work with GHC 6.10, at least. It may work now.

 2. combination with overlapping instances

The type equality predicate is only one example, there are several of
that kind. Just for the record, the following code

        class Eq a b c | a b -> c
	instance Eq k k True
	instance Eq j k False

never worked. (GHC may have accepted the above declarations; that
doesn't mean much since overlapping was detected lazily). The
key insight of HList is the realization why the code above did not
work and how to hack around it (TypeCast or ~ is needed).

If GHC somehow provided Eq as a built-in, that would not have been
enough. We need something like Eq at higher kinds. For example,

	http://okmij.org/ftp/Haskell/typecast.html#is-function-type

That web page gives example of IsList, IsArray and other such
predicates.

The most practical application of overlapping instances is documented
in

http://www.haskell.org/pipermail/haskell-cafe/2010-June/078590.html
http://www.haskell.org/pipermail/haskell-cafe/2010-June/078739.html


The solution has been described already in the HList paper: provide
something the typeOf at the type level. That is, assume a type
function

	TypeOf :: * -> TYPEREP

where TYPEREP is a family of types that describe the type of TypeOf's
argument in the way TypeRep value described the type. The HList paper
(Sec 9) has outlined an ugly solution: associate with each type constructor a
type-level numeral; TYPEREP is a type-level list then, which contains 
the code for the head constructor and TYPEREPs of the arguments.
TYPEREPs are easily comparable.

The HList solution is certainly ugly and non-scalable. The biggest
problem is assigning opaque integers to type constructors and ensuring
the uniqueness. Once I toyed with the idea of defining a family of
types to be the HList of Dot and Dash, so we would spell the name
of the constructor in Morse code.

I must stress that my proposal is rather timid: Matthias Blume, 
when designing a new FFI for SML/NJ has lifted the whole latin alphabet
to the type level:
	http://people.cs.uchicago.edu/~blume/papers/nlffi-entcs.pdf
so he could spell the names of C struct in SML types. This NLFFI has
been used in SML/NJ, in production, for about 10 years. If SML
developers could do that, certainly GHC developers could.


Persistent rumors hold that someone is working on adding more kinds to
GHC. A Kind NAME and a Kind TYPEREP seem good kinds to have (along
with naturals, of course). GHC could then provide the type function
TypeOf. Once we have a TYPEREP, we can compare and deconstruct it,
removing the need for overlapping instances.