TypeFamilies vs. FunctionalDependencies & type-level recursion

[AntC]

 <oleg at ...> writes:
> 
> 
> [28 Jul 2011] ... . Incidentally, I have advocated abolishing Overlapping
> Instances in a short presentation at the 2004 Haskell Workshop (almost
> immediately after Ralf's HList talk).

Hi Oleg, I appreciate it's been a very long time since this thread was active. 
But I think I might have discovered that you and Ralf were premature to reject 
overlaps w.r.t. HList.

The headline news is that I have implemented hDeleteMany in Hugs.

I'm dragging up this ancient history not to argue in favour of fundeps, nor to 
bring Hugs back from its slumbers, but pro a better-implemented approach to 
overlaps (preferably available with Type Families).

To recap the context:

> 
> > [AntC wrote]
> > Selecting instances based on inequalities is already implemented in
> > GHC and Hugs.  (And has been successfully used for over a decade.)
> > You've used it extensively yourself in the HList work, and much other
> > type-level manipulation (such as IsFunction).
Also the original post said:
> > Selecting instances based on inequalities ... got all mixed up with
> > Functional Dependencies ...
> 
> I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping
> instances, and indeed _some_, simple code using overlapping
> instances work the same way in GHC and Hugs. However, HList in
> full does not work in Hugs; ...

The point at which the HList paper "give up on persuading Hugs" was with the 
instance definitions for hDeleteMany [Section 6 'Ended up in murky water'] 
because "There is no real consensus on the overlapping instance mechanism as 
soon as functional dependencies are involved. ... Hugs reports that the 
instances are inconsistent with the functional dependency for HDeleteMany."

There has been a lot of water under the bridge since that interchange. In 
particular, GHC has got type equality constraints mature, with powerful type 
inference. SPJ showed a technique he called "a functional-dependency-like 
mechanism (but using equalities) for the result type". [This was for an 
application where using an Associated Type would not work. So he introduced an 
extra type parameter to the class.]

I noted that HList has an approximation to equality constraints (TypeCast). I 
took the fundep away from HDeleteMany, and instead implemented the instances 
with TypeCast constraints to infer the result type:
1. There's no longer trouble with fundep interference.
2. So you can declare the instances OK (with overlaps well-ordered).
3. The typecast works a dream.

[To be precise, I haven't done away with fundeps altogether, because they 
support TypeCast. And I expect that hDeleteMany without fundeps is not going 
to play well with large-scale programs needing extensive type inference. My 
point is only that it's the interference between fundeps and overlap that 
messes up both.]

We could possibly design a better fundep, but I think fundeps are moribund. 
I'd rather put the effort into introducing overlaps into Type Families, and 
addressing the soundness concerns.

> 
> I don't think Overlapping Instances will be in Haskell' any time soon
> since there are doubts about the soundness. Overlapping
> instances are clearly unsound with type functions. Whether they are
> sound with functional dependencies is not clear, but there are warning
> signs:
> 
> 	http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
> 
> Please see the whole discussion on Haskell-Cafe in July 2010.
> 

I have now studied SPJ's post, and that whole discussion. [Heck, July 2010 had 
some heavy-duty type theory.] I note that one of the threads that month was 
on 'in-equality type constraint's -- which is exactly what I think it needs to 
handle overlapping instances in a disciplined way.  SPJ's post is dense, and I 
think worth replying to in detail, now that we have mature experience with 
equality constraints.

> 
> > I take it the Northern hemisphere is now on academic summer holidays.
> Generally, yes. I wish I had a holiday though...
> 
My timing is again terrible: I suppose Northern Hemisphere academics are 
furiously ending their year and heading for the beach.

AntC