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