On Sat May 13 06:40:47 UTC 2017, mniip wrote3:

...

On Fri, May 12, 2017 at 01:22:35PM -0400, Richard Eisenberg wrote:

...

My interpretation of mniip’s use of this descriptor was

..

That is very much correct, but what I was exactly referring to was not the necessary limitations of type families (such as inability of partial application) but rather their unnecessary limitations. For example only being able to pattern-match at the top-level, or, with InjectiveTypeFamilies, lack of 'result arg1 -> arg2' type injectivity.

Don't we get limited injectivity through type family calls appearing in Equality constraints?

class (F a b ~ c) => C a b c

We might have:

type instance F Int b = b

And a use site which gives (a ~ Int). Then we can improve via (b ~ c).

...

I agree that closed type families are bizarre and perhaps a misfeature -- though I think they are a good incremental step toward something better.

Closed type families have proven very useful to me, ...

Thanks mniip. Yes useful to me too. (As a major user of HList-alikes.)

so I don't agree with calling them a misfeature, ...

I think there were plenty of people suggesting other ways to achieve the same end. If "something better" comes out of the experience, we've lost 7~8 years of opportunity.

however I can see where you're coming from : throughout the entire language we enforce the notion that we can't have a "proof of type inequality" and then closed type families give us just that.

I don't like calling it "type inequality". It's proof of non-unifiability. And the rules for that are easy to write down. (Admittedly a bit messy to apply in practice.) The key fact is that Oleg et al demonstrated how it worked way back in 2004. And it works in Hugs! I don't see what's so hard.

Indeed, their semantics could be made more apparent.

Disequality guards make it blimmin obvious. As described in Sulzmann & Stuckey 2002. AntC