TypeFamilies vs. FunctionalDependencies & type-level recursion

[AntC]

Simon Peyton-Jones <simonpj at ...> writes:

> [from 29 Jul 2011]
> 
> So, let me ask: does anyone (eg Oleg) have concrete proposals on the table 
for things they'd like GHC to do?  
> 
> Arising from the thread, two particular things jump out at me.  ...

The two things are, I think, trying to achieve the same objective. Namely, 
supporting type-level inference driven from a type-level equality predicate.

Of those two things (details continued below), I understand Oleg does have a 
concrete proposal for the first (and a prototype). My proposal earlier in the 
thread was along the lines of your second particular thing. But I delayed 
replying immediately:
- Oleg suggested I refer back to several similar threads in July 2010
        (thank you, that was indeed a valuable discussion)
- GHC has now delivered robust type inference with type equality constraints,
- and superclass constraints.
- And we have the beginnings of data Kinds
- And there has been 'loose talk' of closed Kinds

(To explain that last: I believe the type inference for closed Kinds will need 
a similar mechanism to overlapping instances for TypeFamilies.)

Although this thread is titled FunctionalDependencies, I'm not going to say 
anything about them except that they interfere badly with overlaps, so both 
have got an unfair reputation IMHO.

Thanks to the improvements in type inference, SPJ has shown a technique he 
called "a functional-dependency-like mechanism (but using equalities) for the 
result type". That applies for Type Class instances, and GHC supports 
overlapping for those, so I've used the technique to simulate overlapping 
TypeFamily instances. 
 
> 
> 1.  Support for type representations.  Oleg showed this:
> 
> | I have implemented type-level TYPEREP ...
> 
> 
> 2. Support for overlapping type function equations.  
> 
> There seems no reason in principle to disallow
> 	type instance F where
> 	  F Int = Bool
> 	  F a = [a]
> There is overlap, but it is resolved top-to-bottom.  The only real 
difficulty with this is how to render it
> into FC.  The only decent way seems to me to be to allow FC axioms to do 
pattern matching themselves.  So the FC
> rendering might be
> 	ax32 a = case a of
>                   Int -> F Int ~ Bool
>                   _   -> F a ~ [a]
> That is, the axioms become type-indexed.  I don't know what complications 
that would add.
> 

I favour support for overlapping type function equations, but not exactly that 
approach. I think a major complication from the programmer's point of view is 
that the type function equations would have to be declared all in the same 
place. (I suspect there would be a similar restriction with closed Kinds.)

A complication for type inference is carrying around some representation of 
that case statement, and applying the top-to-bottom inference.

I think it preferable from a programmer's point of view to have separately 
declared stand-alone instances. And I guess this might be easier to manage for 
type inference.

And I propose a form for the instances that achieves the type function above, 
but with what you might call "explicitly non-overlapping overlaps", like this:

        type instance F Int = Bool
        type instance F a | a /~ Int = [a]  -- explicit dis-equality restraint

These can't overlap, because the restraint (aka type-level guard) says "you 
must have evidence that typevar a is not Int before this binding applies". And 
we can validate those instances for non-overlap: the instance heads overlap 
just in case a ~ Int. (I suspect much of this logic is already in place to 
handle overlapping instances. In a 2010 post Oleg gave a very convincing 
characterisation.)

[Something very similar to dis-equality guards was briefly shown in Sulzmann & 
Stuckey. A Theory of Overloading (2002).]

I'm calling these "restraints" because they're not like constraints. 
Restraints block instance matching, whereas constraints validate the instance 
_after_ matching. But the terminology is going to get confusing, because 
inside type inference, I think they'd be implemented as what's 
called "implication constraints" (as used for GADT's).

That second binding gives rise to an axiom:

        (a /~ Int ==> F a ~ [a])    -- using ==> for implication

(The axiom for the first binding is as usual, no implication needed.)


I dislike Oleg's TypeRep approach, because it brings in another layer of 
encoding. I think it would be simpler from a programmer's point of view to 
have types 'standing for themselves'.

I prefer "explicitly non-overlapping overlaps" because the type function 
guards look and behave similarly to guards for function bindings. (But a 
significant difference is that type function instances must be mutually 
exclusive, and that's how come they can be declared stand-alone. The 
requirement to be mutually exclusive means we avoid all that trouble with 
IncoherentInstances and imported overlaps silently changing behaviour -- I 
would explain further, but this post has gone on long enough.)

AntC