[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated
anthony_clayden at clear.net.nz
Thu Nov 28 05:32:52 UTC 2013
> adam vogt <vogt.adam <at> gmail.com> writes:
> > On Wed, Nov 27, 2013 at 9:22 PM, AntC wrote:
> Closed type families ... wait a few weeks for ghc-7.8)
Yes, I'm in eager anticipation!
> > ...
> > OTOH, I did feed raise that unhappy hack with Richard
> > at the time, as a counter-example
> > that I couldn't understand how he'd handle.
> > So perhaps he didn't.)
> Do you recall where that discussion was?
My message on June 24. (It also mentions discussion on GHC-Users.)
This is exactly an example of a records mechanism with duplicate 'labels'.
Actually being what the HList paper calls Type-Indexed Products.
Note that the code I give there works beautifully with old-fashioned
overlapping instances; and produces a helpful error message without any
additional ancillary Fail classes.
It works because my records are tuples, _not_ HLists.
So instance resolution is working with a 'flat' structure where it can see
all the types. Contrast that HCons effectively hides types in its tail.
I suspect that Richard's implementation also effectively hides potential
duplicates by putting them in a later 'case' of the type family.
> ... Though it seems ghc isn't eager enough ...
This is what I find most frustrating with ghc (as contrasted with dear old
Hugs): instance failures are 'lazy'. You have to backtrack through a lot
of code/other modules to figure out what's going wrong.
I was hoping that with Richard's work, instance validation could be eager:
reject the instance definition as overlapping _at_the_point_of_definition_.
I think that a long time ago ghc took a wrong turn and allowed partially
overlapping instances. It therefore has to wait until it finds a usage to
see if it is actually ambiguous.
I think that partially overlapping instances should be banned.
Instances should be either disjunctive or wholly overlapping.
(Note that you can always reorganise a partial overlap to fit this rule.)
> Which translates to
> type family G' x y where
> G' x x = Failure "mistake" ()
> G' x y = ()
That's exactly the unhappy hack I was wanting to avoid.
If you still have to do that with closed type families,
then I'm disappointed.
I wanted disequality restraints.
(See the Sulzmann and Stuckey paper I mention earlier on Richard's
Which would be one single stand-alone instance:
type instance G'' x y | x /~ y = ()
(I also think this has more perspicuous type inference rules,
and fits better with a mental model of all the instances 'competing' to be
chosen at the use site; with type improvement progressing until exactly
one matches. This does not involve instance search, which as SPJ points
out would be death to coherence.)
More information about the Haskell-Cafe