[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