TypeFamilies vs. FunctionalDependencies & type-level recursion
anthony_clayden at clear.net.nz
Tue May 22 12:13:06 CEST 2012
<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
> 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
> > 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.
More information about the Haskell-prime