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

newer
exporting Constructors as...

older
parallel package, rts ROOT vs WEAK...

Anthony Clayden

14 May 2017 14 May '17

9:51 a.m.

...

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

Show replies by date

Richard Eisenberg

15 May 15 May

4:20 p.m.

New subject: [ghc-proposals/cafe] Partially applied type families

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

Zemyla

18 May 18 May

8:59 p.m.

New subject: [ghc-proposals/cafe] Partially applied type families

If partial type families can be a problem, then how do you verify totality, especially considering that Any is a member of every kind, so you might have to check for F Any, F (Any Int), F (Any (Any 7) 'Just), and so on? On Mon, May 15, 2017 at 11:20 AM, Richard Eisenberg wrote:

...

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Richard Eisenberg

19 May 19 May

1:05 a.m.

New subject: [ghc-proposals/cafe] Partially applied type families

Although I am waiting for enough time to adequately respond to AntC's latest volley, I can nab this one:

...

On May 18, 2017, at 4:59 PM, Zemyla wrote:

If partial type families can be a problem, then how do you verify totality, especially considering that Any is a member of every kind, so you might have to check for F Any, F (Any Int), F (Any (Any 7) 'Just), and so on?

Totality is a combination of coverage and termination. It seems you are worried about coverage here -- are all possible patterns considered? However, Any doesn't pose a problem here. Because Any is an empty closed type family, it cannot appear on the left-hand side of a type family instance. (This is a change from how it was, once upon a time. But it's been this way for several releases, I think.) Termination, on the other hand, is a hard nut to crack. I offer no new nutcrackers, I'm afraid. Richard

...

On Mon, May 15, 2017 at 11:20 AM, Richard Eisenberg wrote:

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

2971

Age (days ago)

2976

Last active (days ago)

List overview

Download

3 comments

3 participants

participants (3)

Anthony Clayden
Richard Eisenberg
Zemyla