[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated

[AntC]

> Richard Eisenberg <eir <at> cis.upenn.edu> writes:
> 
> A few reactions to this thread, in no particular order:
>

Thank you Richard for your comprehensive reply.
There's been so much e-ink spilt on the subject over the years,
I don't really want to repeat it, so a few key points (in reverse of your 
order ;-) ...

> - Banning instance overlap that is currently permitted would break 
>   existing code. Is this a big enough wart
>   to incite a breaking change?

Errm, no: overlap is not "currently permitted".
Overlap is not part of H98.
Overlap is not sanctioned as part of H2010.
Overlap is not even on the slate for Haskell Prime.
Its status is clearly marked as experimental/unsafe.
MTL was reorganised to remove Overlap.
There's various trickery in the base classes to avoid overlap.
(Such as showlist.)

That said, I know there's plenty of code out there.
(I've written it myself.)
I think there is very little code with genuinely partial overlaps,
as opposed to total overlaps.
(And total overlaps are easily turned into disequality guards.)

The difficulties that Oleg & Ralf ran into with overlaps,
it turns out can be made to work -- even in Hugs.
That is, if you use overlaps in a very disciplined way.
That way amounts to disequality guards.

I wish I had the time and competence to implement the guards idea.
Then we could experiment with the issues under debate ...


> - While I agree that closed type families don't fit as well with the
>   mental model of competing instances, I believe they work better
>   with programmers' sensibilities at the term level.
>   One could argue which is better to aim for.

So I'm going to argue ;-):
- Guards are already familiar at the term level.
- I'm not convinced that instance selection is ever-so like the term level.
  (For example, you've introduced some look-ahead coincidence-checking,
   to improve the chances for closed families.)
- We're already used to widely-scattered definitions of class methods
  at the term level.
- I'd love Haskell to support widely-scattered definitions of functions
  (It's sometimes a pain to have to put all of the patterns
   together in sequence.)
- (IOW, let's make terms more like instances, rather than v.v.)


> - The notion of "competing instances" for type families sounds somewhat 
> like delayed overlap checks for class instances. ...

No. No delay. The point is to validate eagerly at the point of declaring 
the instance (and whether or not it's in some other module).
The guards guarantee that no instances overlap.
Importing an overlapping instance is trapped immediately;
no risk of incoherence.

Then we know that any usage cannot possibly match more than one instance.
We can let all instances compete.
Whichever one 'wins', we can be sure it's the only one.
(This of course doesn't guarantee there will be a winner at all;
 instance matching can still get 'stuck', as you say.)

> For example, consider these definitions:
> 
> > module A where
> > type instance F a b c | b /~ c = Int
> 
> > module B where
> > import A
> > type instance F a b c | a /~ c = Bool
> 
> Questions:
>   1. Are these instances overlapping?

Yes, so compile fails at the instances. No need to look at usages.
(I gave the rules by which it would fail in some message way back;
 it is algorithmic, and based on what I think is
 existing ghc behaviour for overlaps.)

So your follow-on questions don't apply
>   2. How does `F Int Bool Char` reduce when written in module A?
>   3. How does `F Int Bool Char` reduce when written in module B?
> 

 
> 
> - I don't see how disequality guards would help with error messages.
> 

OK, the example is to check that there's exactly one occurence of a type-
level label in an HList.
This is hard, so Leijen's approach doesn't try.
Having found an instance with the label,
HList uses an auxiliary class `Lacks` to validate that the label doesn't 
appear in the Hlist's tail, like this:

    instance (Lacks lab l') => Has lab (HCons (lab, val) l')

How to code `Lacks`?

    instance Lacks lab HNil     -- got to the end of the tail OK
    instance (Lacks lab l') => Lacks lab (HCons (lab2, val) l')
                                -- not here, recurse on the tail

But that doesn't work! the instance matches even when `lab` is the same as 
`lab2`. We need an extra instance, which we want to treat as failure:

    instance (Fail SomeMessage) => Lacks lab (HCons (lab, val) l')
                                -- repeated typevar  ^^^

Deliberately to trigger the failure, we make sure there's no instance for 
`Fail`. So the compiler error message is 'No instance for Fail ...';
but it _means_ there _is_ an instances for `Lacks`.

With a disequality guards we'd have only one instance:

    instance (Lacks lab l') => Lacks lab (HCons (lab2, val) l')
                                   | lab  /~ lab2

And the compiler message would be
 'No instance for Lacks L1 (HCons (L1, Int) ...)`.
We can see the repeated label.

Now I concede that all this design involves a kinda double-negative.
At least we get focus on the class causing the failure.


AntC