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

[Anthony Clayden]

> On Fri Jun 2 13:48:43 UTC 2017, Richard Eisenberg wrote:

> I'm going to respond just to the few points that concern
> me directly.
>

Thanks Richard, blige! there's a lot to catch up with.
 
> > On Jun 2, 2017, at 9:34 AM, Anthony Clayden wrote: 
> >>> There's a persistent problem for the compiler
> >>> testing for type equality:
> >>> the usage sites must have the types grounded.
> >>> It's often more successful to prove disequality.
> > 
> > That's straight out of the HList paper [2],
> > Section 9 "By chance or by design?".
> >    "We should point out however groundness issues.
> >     If TypeEq is to return HTrue, the types must be
> >     ground; TypeEq can return HFalse even for unground
> >     types, provided they are instantiated enough to
> >     determine that they are not equal."
> 
> While this may be true for HList's TypeEq, it is not true
> for closed type families. If we have
> 
> > type family Equals a b where
> >   Equals a a = True
> >   Equals a b = False
> 

HList's TypeEq is comparable from 2004!,
using typeclasses/FunDeps/Overlaps:

> class TypeEq a b p | a b -> p  where
> instance TypeEq a a HTrue
> instance (p ~ HFalse) => TypeEq a b p

The False instance needs bare typevar `p`
so that it overlaps; consequently needs
UndecidableInstances.
(I've used (~), but that was a typecast class in 2004.)

> then (Equals [a] [a]) will reduce to True, even if `a` is
> universally bound. Indeed, even (Equals a a) will reduce
> to True. So there is no groundness issue any more.
> 

Great stuff! And that TypeEq behaves likewise now.

I was trying to cast the discussion back to ~2010,
the Instance Chains work. IIRC groundedness was
still a difficulty then.

> > 
> >> and also:
> > 
> >>> I suspect that for the compiler,
> >>> Instance Chains will be as problematic
> >>> for type inference as with Closed Type Families:
> >>> CTFs have a lot of searching under the covers
> >>> to 'look ahead' for equations that can safely match.
> > 
> > That's from Richard, particularly this comment [3].
> > The whole blog post is relevant here, I think.
> 
> I'm not sure where you're getting "look ahead" from.
> Closed type families -- and that post, as far as I can
> tell -- don't discuss looking ahead. Instead, closed type
> families are all about looking *behind*,

Well, I think we're saying the same thing.
Your last comment on that blog post
links to the NewAxioms write-up.
That has this example:

> type family And (a :: Bool) (b :: Bool) where
>  And False a     = False
>  And True  b     = b
>  And c     False = False
>  And d     True  = d
>  And e     e     = e

"All of these equations are compatible, meaning that GHC
 does not have to do the apartness check against the
target."

Faced with simplifying `And c False`,
does GHC get stuck at the first or second equation,
because it can't resolve `c` to `False` or `True`?
No, it "looks ahead" to the third equation.
Because it sees that if `And c False` unifies
with either of the first two,
it'll yield the same result `False`.

Your comment on the blog post is
"coincident overlap within closed type families
 (the new nomenclature for branched instances)
 would indeed be useful."

I think it would be useful, too, for Instance Chains
or Closed Classes. But there's a problem:

Class instances must select method implementations,
as well type improvement.
So we need to fix on a specific instance,
even though we only have `And c False`.

> > I think the situation has changed with the introduction
> > of Type Families. They weren't applicable in 2010.
> > So not relevant to the Instance Chains paper.
> 

My mistake: I meant to say "... introduction of Closed Type
Families".

> Type families were introduced in 2005, I believe.
> At least, that's when the papers were written. 

Hmm, careful. 2005 was Assoc types only.

The usually cited paper for Type Families
is Schrivers et al 2008.
Garrett's papers cite that, not the 2005,
and I agree that's the full write-up.
But the 2008 paper was written in parallel with development.
The feature appeared in GHC after the paper.
And it wasn't complete:
we waited a long time to get Type Families/(~)
in superclass constraints.
(There were a couple of release which supported the syntax
 superclass, but it did nothing.)

> I don't know what version of GHC first included them,
> but I think it was before 2010.
> 

Vintage ~2010 there was limited support for overlap
in TF instances -- the equations had to be "confluent".
(This is the (||) example near the top of your blog post,
 where you conclude "and we can just write || using separate
instances, anyway."
 Yes you could just write separate instances in ~2010.)

I don't see that Instance Chains has a comparable notion
of "confluent" or "compatible".
But perhaps I missed it.

> > 
> > "Look ahead" is exactly what Richard is describing
> > in the bulk of that blog post.
> 
> I disagree here: ...

See above


AntC