On Wed May 24 02:33:46 UTC 2017, Richard Eisenberg wrote:

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

Thanks Richard, yes I think we have large areas of agreement. So I'll cut to where we differ.

...

On May 15, 2017, at 9:26 PM, Anthony Clayden 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.

Then I guess I remain to be convinced of the value of dependent typing within Haskell.

...These languages still do multi-directional type inference,

I guess you mean as needed for superclass constraints and instance constraints, so perhaps there's no practical difference.

...

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.

I'd like term-level functions to be more like instances. That is, with the equations distributed, see your example below. (Yes the set of equations must be coherent overall. That's something the compiler can check for me.)

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.

Yes.

...

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

Oh, yes I think a lot of people are confused. I think they expect the second equation is equivalent to:

f (x:xs) = True

Maybe even

f ~(x:xs) = True

But in the presence of bottom, that's a dangerous delusion. I'd say: if you want the True result to mean there's a non-empty list, then put that explicitly. And then we have two equations that are 'apart'. And they don't need to be sequential. Furthermore that delusion is doubly dangerous for type equations, because GHC knows nothing of closed Data Kinds.

...

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.

No, you're not repeating old arguments. Type Families, and esp. CTFs really came later. IIRC, at the time, there was a lot of suggestions, but not much push-back from anybody disagreeing. There was some doubt whether there could be a type-level disequality test. Chiefly GHC HQ just ignored the whole thing. Somebody at the time did try to write it up (viz. moi) https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage And someone from GHC HQ (viz. you) did acknowledge it rather later.

...

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.

OK I think you're saying that a class decl with superclass (~) constraints to type functions is preferable/more aesthetic. I agree. Furthermore overlap interferes with fundeps (or perhaps I mean v.v.) in horrible ways.

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

Yes I can see the dangers of confusion. We could of course use a different operator.

... They're different, but I think the equality guard is useless

I see two main uses/benefits: 1. avoids the need for non-linear patterns in the head 2. visually points up the 'non-apartness' vs an, um. "apartness guard" (When I was figuring out Andy A-M's 2013 example, I rewrote the non-linear patterns with ~ guards, so I could figure out the apartness guards esp for the semi-apart instances. I posted the later workings to your blog https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-fa... )

[except as a type-level "let", I suppose].)

No, they're not doing that: deliberately I don't allow guards to introduce new type vars.

... partial type families ... 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.

Yes I got that loud and clear, and I agree. So the remaining issue is _how_ to protect them.

...

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/CustomType Errors, which is now available in GHC 8).

Ok thanks, yes that helps. Nevertheless it seems disergonomic to write an instance for a type-equal case, even with a helpful error message; when what you want is: no such instance.

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.

I've been (mostly in my head) calling them "Instance Guards", because I want both an eq guard and an apartness guard.

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.

Yes that's what I guessed from your write-up of CTFs and "coincident overlap". What I can see will be awkward is backwards compatibility: can a class/type family with guards coexist with CTFs and with classes using overlap?

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

I'll have a crack at the proposal. But implementing it is entirely beyond me. So thanks for saying "you win". But I'm not celebrating 'til something actually happens. (Been bitten too many times.) AntC