TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

First of all, I do agree with David. Overlapping instances are indeed
very useful in practice, cutting down significant amount of
boiler-plate. His examples, as well the example from polymorphic map
libraries (mentioned earlier) are real-world cases where overlapping
instances are invaluable and indispensable.


I do wish to point out the need for `proper credit': is the benefit
specifically because of overlapping, or functional dependencies alone
suffice? As far as I noticed, all compelling examples used and
relied on overlapping instances (not just functional dependencies or
undecidable instances)

The functional dependencies per se are quite well understood: see

	The theory of overloading
	Peter J. Stuckey and Martin Sulzmann
	TOPLAS, 2005, v27, N6, 1216--1269
	http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.837
	(perhaps there is a better URL, to the final version of the paper)

	Language and Program Design for Functional Dependencies
	Mark P. Jones, Iavor S. Diatchki
	http://web.cecs.pdx.edu/~mpj/pubs/fundeps-design.html


`The theory of overloading' should answer Dan Doel's question about the
ideal way of handling functional dependencies. The paper should
also answer all of David's questions about functional dependencies,
explaining why Iavor and I so object to
	class C a b | a -> b
	instance C a b


It is the overlapping instances that muddy the water (especially in
combination with other Haskell features such as higher-rank
types). There is a nagging feeling that the combination may even be
unsound. But the overlapping instances are so useful and compelling!
That is exactly the problem that started this thread, as I understand.


I do wish to stress the solution I have proposed earlier. I think it
helps implement all of David's examples (and all of mine examples),
without overlapping instances. Whether one uses functional
dependencies or type functions is a secondary, and minor issue.
The solution could be implemented (in ugly way) even now, but will
benefit from _small_ GHC support. There are NO changes to GHC core or to
the FC calculus are required. 


David wrote:
>     class C a b | a -> b where
>        aDefault :: a
>        aTobC :: a -> b
>     class D a b where                     -- no fundep
>        aTobD :: a -> b
>     instance (D Int b) => C Int b where   -- should this be allowed?
>        aDefault = 0
>        aTobC = aTobD
>
> 	class C' a b | a -> b
> 	class E a b | a -> b       -- unlike above, we now have a fundep
> 	instance (E a b) => C' a b
>
> Oleg, you haven't weighed in this specific question, but I think many
> of your ideas require the ability to write instances like C', even if
> you advocate disallowing C.

I would argue for rejection of the instance of C but accepting C'. The
Prolog program posted yesterday will back me up. 

I should stress the underlying reason. First of all, when considering
if an instance violates functional dependency, the methods of the
instance are irrelevant. Only the instance head and its constraints
matter. Here is why. Recall the main property:

	(C a b1, C a b2) ==> b1 ~ b2

Here is the corollary: given
	instance C Int Bool
and the type 
	forall t. C Int t => t

we _improve_ the type to just Bool. The type equality constraint 
t ~ Int lets us replace all occurrences of the variable t with Int. This
is exactly the sort of substitution that underlies
lambda-calculus. Thus, the process of improvement simulates general
computation. Thus functional dependencies let us write and run
type-level programs.