[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
anthony_clayden at clear.net.nz
Sat May 13 11:12:02 UTC 2017
> On Sat May 13 06:40:47 UTC 2017, mniip wrote3:
>> On Fri, May 12, 2017 at 01:22:35PM -0400, Richard
>> 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
> being able to pattern-match at the top-level, or, with
> InjectiveTypeFamilies, lack of 'result arg1 -> arg2' type
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
>> -- though I think they are a good incremental step toward
> 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
> 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.
More information about the Haskell-Cafe