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 mniips 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