[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families

[Richard Eisenberg]

> On May 15, 2017, at 9:26 PM, Anthony Clayden <anthony_clayden at clear.net.nz> wrote:
> 
> "Multidirectional type-level reasoning" is what all
> functional languages do: from Robinson's unification
> to Hindley-Milner to OutsideIn(X)
> to System F-subscript-superscript.

I disagree here: the dependently typed languages don't quite do this. For them, a type-level function is just that: it has an input that determines the output. These languages still do multi-directional type inference, but not all parts of their type system play so nicely with the multi-directional part.
> 
> I think we can mechanically translate closed equations
> to guards (equality and 'apart' tests).
> The example in my earlier post
> tried to show how.

Agreed.

> 
> For class instances (with overlaps),
> I think there's also a mechanical translation,
> but only for 'well-behaved' sets of instances.
> (For Incoherent sets we don't have a chance.)
> And of course as soon as some imported instance overlaps,
> we have to start again to assess well-behavedness.

Agreed.
> 
> The backwards-compatibility I particularly
> want to preserve is "distributed instances".
> That is, putting the instance code
> close to type decls and other functions that 
> build or consume that type.

I think one other key difference between our viewpoints is that I view the whole idea of "type instance" to be a bit backward: I view type families as type-level functions. Like other functions, I want the defining equations to be all in one place. Of course, class methods are distributed in exactly the same way as type instances, but most of my work with type families has not needed the distributed aspect of them.

This isn't to argue that my viewpoint is right or that other viewpoints are wrong. It's just a way to understand why we both see things the way we do.

> I'd argue it's simpler to understand each instance
> on its own grounds.

Permit me to rewrite your sentence to something that resonates better with me:

> I'd argue it's simpler to understand each *equation*
> on its own grounds.

I agree here, but it's a bit subtler. We aren't confused when we see

> f [] = False
> f _  = True

even though the meaning of the second equation crucially depends on it appearing after the first. Functional programmers are used to ordering like this. But when things get more complicated, perhaps you're right.
> 
> There was a huge and rather repetitive (unfortunately)
> discussion
> in several rounds 2009~2012,

These dates might help to explain why I may be repeating old arguments. I became active in the community somewhere in 2012.
> 
> I'm a little unsure what you mean at the top of the post
> about the "idea" of FunDeps vs their specific syntax.

By "idea", I mean traits like multidirectionality and attachment to classes. I maintain that the function-application syntax of type families is better than the relational syntax of fundeps.

> A set of instances is well-behaved wrt overlap
> iff for each pairing of instances, one of:

Thanks for this analysis. I agree.

> Rules for guards:
> a) The guards are a comma-sep list
>    of equal (~) or apart (/~) comparisons.
> b) The comparands must be same-kinded.
>    (I'll leave the poly kinded case for Richard ;-)
> c) Can only use type vars from the head.
>    (I.e. not introduce extra vars, which contexts can do.)
> d) No type functions -- too hard, and not injective.
> e) Can use wildcard `_` as a type place-holder.
> f) Can use Type constructors to arbitrary nesting.

I agree here, too, though I'm not sure we need to allow ~ guards. (I think allowing them would cause confusion, with many people asking about the difference between an equality constraint and an equality guard. They're different, but I think the equality guard is useless [except as a type-level "let", I suppose].) 

>> The key observation is this: partiality in types is
> bizarre, and we don't want it. ...
> 
> Huh? Nearly all type families (and class instances) are
> partial. 
> You perhaps mean "don't want it" as purist
> type-theoreticians(?) 

Partial type families (including non-terminating ones) are bizarre because they cause wrinkles in the fabric of type families. Some of the strangeness of closed type families (Section 6 of the original Closed Type Families paper) and all of the strangeness of injective type families are caused by partiality. So I dislike partial type families for very practical reasons. Of course, when you protect a partial type family by a class constraint, then it's not troublesome: that's the point of the Constrained Type Families paper.

> Sometimes I deliberately want there to be no instance
> for some specific pattern. 

Indeed yes. And now you can, with TypeError (https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors, which is now available in GHC 8). The problem with instance chains is their backtracking capability, but we can have failure without backtracking.

> Errk I see a fly in the ointment with these
> 'closed classes'/associated types. Suppose:
> 
> A class with two assoc types
> * One assoc type needs the instances in a specific sequence.
> * The other assoc type needs the instances in a different
> sequence.
> 
> Here's a simple (as in daft!) example:

Hm. Interesting, illustrative example.

Bottom line: You win. I'm convinced. Apartness guards (feel free to fight me on the name here -- I don't feel strongly, but somehow I like "apartness guards" more than "disequality guards") subsume OverlappingInstances (when the author of the instances has a particular desired way to resolve overlap) and closed type families. I think that the syntax of closed type families is often what the user wants, but I admit that CTFs don't cover all scenarios, especially in the context of Constrained Type Families. So I think we should keep CTFs (for now -- until Dependent Haskell is here) but add this new syntax as well, which would subsume the newly-proposed closed type classes.

Even better, I think apartness guards would be very easy to implement. All the plumbing is already installed: we basically just have to add a switch.

Next step: write a ghc-proposal. I'll support it. If I had the time, I'd even implement it.

Thanks for getting me to think about all this in a new way!

Richard