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

[Anthony Clayden]

> 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