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

[Anthony Clayden]

> 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-families/#comment-712
)



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