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

[Anthony Clayden]

> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote:

> 
> > On May 12, 2017, at 6:46 AM, Anthony Clayden wrote: 
> > So please explain here in what way 
> > type families are "half baked".
> 
> My interpretation of mniip's use of this descriptor was
> a reference to the fact that type families aren't just
> functions, don't support `case`, ...

?? But the instance mechanism is in effect case;
only considerably more powerful:
 
> I agree that closed type families are bizarre and perhaps
> a misfeature -- though I think they are a good incremental
> step toward something better. What would be far better is
> if we could just use `case`, and then the closed type
> family syntax would desugar into case statements, much
> like how normal functions work. So 
> 
> type family F a b where
>   F Int b    = b
>   F a   Bool = a
> 
> (AntC's example) would really mean
> 
> type F a b = case a of
>   Int -> b
>   _   -> case b of
>            Bool -> a
>            _    -> F a b
> 

But this is terrible for type improvement!:
It insists on working through the args
left to right. And through the equations
top to bottom.

Contrast all the good work Richard did
for closed families, to 'look ahead',
detect confluence of equations,
and try to make progress in solving equations. 
As described here
https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/
and in the 2013 paper.

i.e. to mimic the behaviour of stand-alone instances.

> We understand the semantics of case expressions, ...

At the term level yes.
But that semantics is not appropriate at the type level.
Type-level programming is somewhat like term level;
but quite a lot different.

At the term level, we never expect to
'improve' an argument from knowledge of the result.

So expecting them to behave the same,
or deliberately hobbling type improvement
to be like term-level case expressions
is just not ergonomic.

What's so difficult to understand about instances?
The worst mis-feature for me about closed families,
is I have to put all the instances together,
not alongside the corresponding class instances
-- even as associated types.

'Grounding' type instances with methods,
and therefore with class instances seems to be a Good Thing,
according to these musings
https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/

Closed families aren't extensible
when I declare a new type.

The part of the (class) instance mechanism
that's difficult to reason about is overlaps.

So the idea of the (dis)equality guards on instances
-- which can apply to class or type instances -- 
is to remove overlaps: essentially,
if the heads overlap (are unifiable),
the guards must disambiguate
which instance to choose.
I can't introduce in a different module
an instance that overlaps.

AntC