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

[Anthony Clayden]

> On Tue May 30 19:43:30 UTC 2017, Richard Eisenberg wrote:

> > On May 24, 2017, at 3:13 AM, Anthony Clayden wrote: 

> ... Some functions are defined by an ordered set of
equations.
> Some (that is, class methods) are defined by
> an unordered set of equations, perhaps distributed across
modules.
> Both models are useful.

Sure. Let a 100 schools of thought contend.

>>> ... [equality constraints and equality guards are]
>>> different, but I think the equality guard is useless
>>
I agree adds nothing over repeating the typevar.
And I've already agreed the potential for confusion with (~)
constraints.
So noted. I'll include it in the proposal,
where a wider audience can bikeshed.
 
>> I see two main uses/benefits:
>> 1. avoids the need for non-linear patterns in the head
> 
> Agreed that it would do this. But why is that important?
>
I was in part thinking of your wondering-out-loud
earlier in the Partially applied thread
https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127078.html

If we want to part-apply a type Fun
which has a non-linear lhs,
how does that go with your case-equation style?

Adapting that earlier example:

> type family F a b where
>  F a   a   = ()     -- added an equation
>  F Int b    = b
>  F a   Bool = a

would really mean

> type F a b = case a of
>  _   -> case b of   -- ?? _ match-all
>        a -> ()     -- ?? re-using typevar a
>  Int -> b
>  _   -> case b of
>           Bool -> a
>           _    -> F a b

 
> > 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
> 
> Somehow, this is more convincing. But I'm still not
> convinced on this point. Happily, you don't need to
> convince me -- put in the proposal what you like and then
> we can debate a concrete design.
> 
> >> [except as a type-level "let", I suppose].) 
> 
> They would work as "let", I think:
> 
> > instance Either a a | a ~ SomethingBigAndUgly where ...
> 
> Note that the `a` is not introduced in the guard.

Ah, OK. I get you. Equally that could be

> instance Either a b | a ~ b, a ~ SomethingBigAndUgly where
..

> 
> > Ok thanks, yes [TypeError] 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.
> 
> You could always view
> 
> > instance TypeError ... => C Int Bool
> 
> as sugar for
> 
> > instance C Int Bool fails

Yes I understand that.
But no I don't want any instance.
(Sugar on rotten fruit doesn't hide the smell.)
There are (or at least used to be) all sorts of
side-effects from there in effect being an instance that
matched.

> > 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?
> 
> Sure. There would be no problem with this. The new idea is
> just that: new. I don't see it as getting rid of anything
> we already have. Perhaps some day we could think about
> removing OverlappingInstances, but we certainly don't have
> to do that at the same time as introducing instance
> guards. (I do like that name, too.)
> 

OK. Perhaps you're seeing something I can't.
To adapt your example from a parallel message, suppose:

> module A
>
>   class {-# INSTANCEGUARDS #-} C a where ...
>   instance C (Maybe a) | a /~ Int where ...
>   instance C (Maybe Int) where ...
>
> module B
>   -- knows nothing of InstanceGuards
>   import A
>
>   instance {-# OVERLAPPABLE #-} C (Maybe Bool) where ...

I want to reject that `(Maybe Bool)` instance.
Even though it would legitimately be OVERLAPPABLE
by (Maybe a) (that is, without the `a /~ Int` guard).
Furthermore I might want a class to be InstanceGuarded,
even though the instances I declare don't themselves need
guards.
(That is, I'm wanting to avoid 'future' overlaps
 in modules that import the class.)

> > 
> > I'll have a crack at the proposal.
> 
> Great. Thanks!

(Likely I'll need some help with the protocols.)


AntC