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

[Richard Eisenberg]

A few reactions to this thread, in no particular order:

- Atze, thanks for doing this work! Powering extensible records was one of the use cases I had for closed type families in the back of my head, and I'm glad someone is going ahead with this!

- Closed type families, as implemented, do nothing to help with error messages that are produced by missing instances (class or type family) or missing equations of a closed type family. For a type family, if no instances/equations are applicable, the use of the type family is "stuck" -- it doesn't reduce. Detecting stuckness using an in-language mechanism risks type safety, because stuckness might change either with type improvement or (in the case of open families) by the inclusion of another module.

- It is conceivable that further work can make closed type families better in this regard. For example, I could imagine a check on the use site of a closed type family that could tell that the use would *never* reduce, regardless of any type improvement that might take place. I can also imagine implementing a customizable error message to use in that case. However, these additions aren't on my current docket of work. I'd be happy to point the way forward to someone else who is interested!

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

- The notion of "competing instances" for type families sounds somewhat like delayed overlap checks for class instances. 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?
  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?

Pondering the answers to these questions makes me doubt this approach.

On the other hand, perhaps we could require that all instances of a type family that have disequality guards are given in the same module. Then, the reduction of something like `F Int Bool Int` is hard to figure out. In short, I'm not sure what is gained by this approach.

(Disclaimer: it is easy enough to find very counter-intuitive examples using closed type families as implemented. I ask these questions more to ponder what an alternative might look like than to say that closed type families are perfect.)

- 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.

- Banning instance overlap that is currently permitted would break existing code. Is this a big enough wart to incite a breaking change? Also, what would happen if two different packages define instances (mainly for internal use) that conflict? These instances would necessarily be orphans. Could these packages then be used together? Perhaps this case never comes up in practice, but it would worry me.

Richard

On Nov 28, 2013, at 12:32 AM, AntC wrote:

>> 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? 
> 
> http://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-
> families/
> 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 
> discussion page.)
> 
> 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.)
> 
> Cheers
> AntC
> 
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe