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

[Richard Eisenberg]

Lots to respond to!

I do think think there's one overarching question/theme here: Do we want functional dependencies or type-level functions? Behind AntC's arguments, I see a thrust toward functional dependencies. (Not necessarily their *syntax*, but the idea of type improvement and flexible -- that is, multidirectional -- type-level reasoning.) My dependent types work pushes me toward type-level functions.

But I think we can have our cake and eat it too. See my recent draft paper (expanding on the "What are type families" blog post) here: http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf  (This paper will appear in revised form at ICFP'17.) While the paper skirts around the issue somewhat, it's really proposing dropping type families in favor of functional dependencies -- but only for partial type families. The key observation is this: partiality in types is bizarre, and we don't want it. So, any time we use a partial type family, you need to have a class constraint around. The class constraint ensures that we evaluate the type family only within its defined domain. Now tied to classes, partial type families are more like convenient syntax for functional dependencies. There is also treatment of partial closed type families via a new construct, closed classes (somewhat like instance chains but weaker).

I expect AntC would prefer disequality guards over closed classes. I would be interested to hear more from the community on this choice -- they're really the same as ordered equations under the hood, and it's just a choice of syntax. Maybe we can even have both.

Now, on to individual points:

> But this is terrible for type improvement!:

I agree that desugaring to `case` expressions would harm type improvement. But it gives us a reliable semantics for type-level computation, something that is sorely lacking today. Can we reconcile these? Perhaps, but it will take some Hard Thought. In any case, any real implementation of these ideas would require the Hard Thought in order to be backward compatible. (This backward compatibility necessity is one of the reasons I love working with Haskell. When adding a feature to the language, we just can't take easy ways out!)

> Closed families aren't extensible
> when I declare a new type.

Quite true, but it's easy enough to make an open type family that calls a closed type family. In the design of closed type families, we originally thought to have (what I called) branched instances, separating out the "closedness" with the overlapping equations. In the end, it seemed simpler to have closed families have the overlapping equations and dispense with branches instances. The big problem with branched instances is that it was awkward to describe the overlap between two branched instances. AntC might argue that, if we just had disequality guards, it would all be much simpler. He might be right.

In retrospect, it would have been nice to have the proposals process active when designing closed type families; we might have come up with a better design.

>> so I don't agree with calling [closed type families] 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.

By "misfeature", I didn't mean that I shouldn't have added closed type families. I'm more referring to some of the oddities pointed out in my draft paper linked above. My recollection at the time is that other approaches were more functional-dependency-like in character. (To wit: instance chains.) When I did the closed type family work, I was thinking that type families were better than functional dependencies; now, my view is much more nuanced (leaning strongly toward fundeps instead of partial type families).

I'm not sure what you mean by "lost 7~8 years of opportunity".

> I don't like calling it "type inequality".
> It's proof of non-unifiability.

I call it apartness!

> I don't see what's so hard [about non-unifiability].

It's not nearly as hard from a fundep point of view. That's because there's a very key difference in fundep-land. Suppose we have

> type family F a where
>   F Int = Bool

and that's it. We can still use `F Char` in a type, even though it's nonsensical. Similarly, if a type family doesn't terminate, we can use the type family at a type that causes it to loop. If we translate the type families to fundeps, these problems go away (say, to `class C a b | a -> b; instance C Int Bool`), because a function with a type that mentions `C Char a` can never be called, as there is no `C Char xyz` instance. The key mistake behind the closed type families paper is, essentially, to assume that `F Char` is a type; all the apartness gobbledegook follows. In my draft paper, we reverse this assumption, cleaning up this theory quite nicely.

> 5.13.2 says: "they [equality testing rules] cannot handle
> the case where Equals a a reduces to True,
> where a is locally bound type variable."
> 
> ?? I thought GHC's equality test
> requires types to be grounded,
> i.e. not merely type vars,
> in order to be judged equal.
> Or did that change recently?


No change here -- since the advent of closed type families, GHC has been able to reduce equality over non-ground types. That's the trouble.

> Isn't that to do with impredicativity
> and the dreaded monomorphism:
> the same typevar might get a different
> forall-qualified type in different use sites.

Not sure what you're talking about here. GHC is resolutely predicative (in this manner, at least -- a logician would be highly flummoxed that we call a system with Type :: Type predicative!).


I do have to say all this talk has made me think more about apartness constraints in FC, at least. They might be a touch simpler than the current story.

Richard


> On May 14, 2017, at 5:51 AM, Anthony Clayden <anthony_clayden at clear.net.nz> wrote:
> 
>> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote:
> 
>> 
>> ... [in] closed type families. (We
>> would also have to eliminate non-linear patterns,
>> replacing them with some other first-class test for
>> equality.
> 
>> AntC's proposed disequality constraints then become
>> straightforward pattern guards.
> 
> Guards don't have to be just disequalities.
> 
> If you want to eliminate non-linear patterns,
> use _equality_ guards. Full example:
> 
>> type family F a b where
>>  F a   a    = a
>>  F Int b    = b
>>  F a   Bool = a
>> 
> 
> Translates to:
> 
>> type instance F a b | a ~ b = a
>> type instance F a b | a ~ Int, a /~ b = b
>> type instance F a b | b ~ Bool, a /~ Int, a /~ b = a
> 
> (Each instance after the first
> has disequality guards to negate the earlier instances'
> equalities., i.e. the earlier instances 'shadow' the
> overlap.)
> 
>> It's currently unclear to me how to do this
>> right. ... 
>> 
> 
> Assuming we have a primitive type-level
> equality test (?~), returning type-level Bool;
> we can use helper functions.
> The first instance desugars to a call
> 
>> ... = F_a_b_Eq (a ?~ b) a b
> 
>> type instance F_a_b_Eq True a b = a
> 
> (Needs UndecidableInstances.)
> 
>> Section 5.13.2 of my thesis dwells on this, without
>> much in the way of a concrete way forward.)
> 
> We use type equality testing all the time.
> In fact instance selection relies on it.
> 
> 5.13.2 says: "they [equality testing rules] cannot handle
> the case where Equals a a reduces to True,
> where a is locally bound type variable."
> 
> ?? I thought GHC's equality test
> requires types to be grounded,
> i.e. not merely type vars,
> in order to be judged equal.
> Or did that change recently?
> 
> Isn't that to do with impredicativity
> and the dreaded monomorphism:
> the same typevar might get a different
> forall-qualified type in different use sites.
> 
> Contrast types can be judged dis-equal
> without necessarily being grounded.
> [HList paper section 9 refers.]
> 
> 
> AntC