#547: Remove kind constraints, Recommendation: accept

older
GHC2023

Arnaud Spiwack

14 Nov 2022 14 Nov '22

5:28 a.m.

Dear all, Our own Richard and Simon PJ are proposing to remove kind constraints from GHC https://github.com/ghc-proposals/ghc-proposals/pull/547 What are they? Well, exactly. It is a little known feature that you can add constraints in kinds. Actually, you can only have equality constraints (e.g. a~Boo => t -> Type (I actually wanted to write Bool, but I decided to keep the typo in honour of the season)), class constraints are already forbidden. The feature is of limited use because you are not allowed to actually use the constraint when writing instances of such a kind. It's purely a restriction (much like data type contexts). Richard describes the feature as having been implemented because it was easy, not because it was answering a particular need (though it is possible to find applications). Richard and Simon have a problem with this not-very-useful feature: its mere existence makes their plan to properly separate Constraints and Types in Core much harder. So they want to just get rid of it. Now, it's difficult to estimate how much this feature is actually used. As we've learnt the hard way with the simplified subsumption proposal. I'd honestly be surprised if there was actually no usage of kind constraints in the wild. So there is always a risk. But I think that this is a fairly safe bet that very few people have actually used this feature. On the other hand the Constraint/Type separation is long overdue. It seems to me that removing the feature is the right call. I recommend acceptance. /Arnaud

Attachments:

attachment.html (text/html — 1.8 KB)

Show replies by date

Joachim Breitner

14 Nov 14 Nov

6:51 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

Hi, Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack:

...

I recommend acceptance.

authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Arnaud Spiwack

17 Nov 17 Nov

5:20 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

...

authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur.

😀 To clarify: the main question is whether we are confident that it won't break too many users. I don't have divination powers that make my word particularly trustworthy on this point. Yet, I do feel pretty confident. On Mon, 14 Nov 2022 at 12:51, Joachim Breitner wrote:

...

Hi,

Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack:

...
I recommend acceptance.

authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur.

Cheers, Joachim

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Arnaud Spiwack

21 Nov 21 Nov

3:32 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

Not many opined. Unless there is opposition, I'll mark the proposal as acceptable sometime before the end of the week. On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack wrote:

...

...
authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur.

😀

To clarify: the main question is whether we are confident that it won't break too many users. I don't have divination powers that make my word particularly trustworthy on this point. Yet, I do feel pretty confident.

On Mon, 14 Nov 2022 at 12:51, Joachim Breitner wrote:

...
Hi,

Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack:

...
I recommend acceptance.

authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur.

Cheers, Joachim

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Adam Gundry

22 Nov 22 Nov

4:31 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

I'm not extremely worried about removing equality constraints in kinds themselves, but I am slightly worried that this proposal will unexpectedly prevent (existing) uses of GADTs with DataKinds. If I understand correctly, this version of MkT will be usable in types: data T a where MkT :: Bool -> T Bool but this will not (even though it could be rewritten to the former): data T a where MkT :: a ~ Bool => Bool -> T a Moreover, this MkT not be usable in types at all: type family F a data T a where MkT :: F a ~ Bool => Bool -> T a I suppose we can live with this in exchange for the gain in simplicity, especially as there seems to be agreement that maintaining the feature is simply too costly. But I would not be all that surprised if some users' code breaks as a result. Cheers, Adam On 21/11/2022 08:32, Arnaud Spiwack wrote:

...

Not many opined. Unless there is opposition, I'll mark the proposal as acceptable sometime before the end of the week.

On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack mailto:arnaud.spiwack@tweag.io> wrote:

> authored by Richard and Simon, and double-checked by Arnaud, I’m happy > to concur.

😀

To clarify: the main question is whether we are confident that it won't break too many users. I don't have divination powers that make my word particularly trustworthy on this point. Yet, I do feel pretty confident.

On Mon, 14 Nov 2022 at 12:51, Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

Hi,

Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack: > I recommend acceptance.

authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur.

Cheers, Joachim https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 27 Old Gloucester Street, London WC1N 3AX, England

Arnaud Spiwack

24 Nov 24 Nov

4:22 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

Adam makes an excellent point. GADTs defined with explicit equality constraints and then promoted is likely to be the main reason for breakage. If only because programmers doing that would probably not even really be aware that they are using constraints in kinds. On the other hand, I don't think that it's super common to defined a GADT that way, so the number of promoted GADTs will be small. Adam, do you nevertheless support acceptance? Does anybody else have an opinion? I intend to mark the proposal as accepted tomorrow unless there is clear opposition. On Tue, 22 Nov 2022 at 10:32, Adam Gundry wrote:

...

I'm not extremely worried about removing equality constraints in kinds themselves, but I am slightly worried that this proposal will unexpectedly prevent (existing) uses of GADTs with DataKinds. If I understand correctly, this version of MkT will be usable in types:

data T a where MkT :: Bool -> T Bool

but this will not (even though it could be rewritten to the former):

data T a where MkT :: a ~ Bool => Bool -> T a

Moreover, this MkT not be usable in types at all:

type family F a data T a where MkT :: F a ~ Bool => Bool -> T a

I suppose we can live with this in exchange for the gain in simplicity, especially as there seems to be agreement that maintaining the feature is simply too costly. But I would not be all that surprised if some users' code breaks as a result.

Cheers,

Adam

On 21/11/2022 08:32, Arnaud Spiwack wrote:

...
Not many opined. Unless there is opposition, I'll mark the proposal as acceptable sometime before the end of the week.

On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack mailto:arnaud.spiwack@tweag.io> wrote:

> authored by Richard and Simon, and double-checked by Arnaud, I’m happy > to concur.

😀

To clarify: the main question is whether we are confident that it won't break too many users. I don't have divination powers that make my word particularly trustworthy on this point. Yet, I do feel pretty confident.

On Mon, 14 Nov 2022 at 12:51, Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

Hi,

Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack: > I recommend acceptance.

authored by Richard and Simon, and double-checked by Arnaud, I’m happy to concur.

Cheers, Joachim https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890 27 Old Gloucester Street, London WC1N 3AX, England

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Adam Gundry

25 Nov 25 Nov

3:57 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

On 24/11/2022 09:22, Arnaud Spiwack wrote:

...

Adam makes an excellent point. GADTs defined with explicit equality constraints and then promoted is likely to be the main reason for breakage. If only because programmers doing that would probably not even really be aware that they are using constraints in kinds. On the other hand, I don't think that it's super common to defined a GADT that way, so the number of promoted GADTs will be small.

Adam, do you nevertheless support acceptance? Does anybody else have an opinion? I intend to mark the proposal as accepted tomorrow unless there is clear opposition.

Yes, I'm okay with acceptance. As you say, this is not the most common way to define GADTs, and given that (a) any class context prevents use in types, and (b) dependent pattern matching on GADTs doesn't work in type families anyway, it seems best to take the simple position that any context at all prevents use of a data constructor in a type. Cheers, Adam

...

On Tue, 22 Nov 2022 at 10:32, Adam Gundry mailto:adam@well-typed.com> wrote:

I'm not extremely worried about removing equality constraints in kinds themselves, but I am slightly worried that this proposal will unexpectedly prevent (existing) uses of GADTs with DataKinds. If I understand correctly, this version of MkT will be usable in types:

data T a where MkT :: Bool -> T Bool

but this will not (even though it could be rewritten to the former):

data T a where MkT :: a ~ Bool => Bool -> T a

Moreover, this MkT not be usable in types at all:

type family F a data T a where MkT :: F a ~ Bool => Bool -> T a

I suppose we can live with this in exchange for the gain in simplicity, especially as there seems to be agreement that maintaining the feature is simply too costly. But I would not be all that surprised if some users' code breaks as a result.

Cheers,

Adam

On 21/11/2022 08:32, Arnaud Spiwack wrote: > Not many opined. Unless there is opposition, I'll mark the proposal as > acceptable sometime before the end of the week. > > On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack mailto:arnaud.spiwack@tweag.io > mailto:arnaud.spiwack@tweag.io>> wrote: > > > authored by Richard and Simon, and double-checked by Arnaud, I’m > happy > > to concur. > > 😀 > > To clarify: the main question is whether we are confident that it > won't break too many users. I don't have divination powers that make > my word particularly trustworthy on this point. Yet, I do feel > pretty confident. > > On Mon, 14 Nov 2022 at 12:51, Joachim Breitner > mailto:mail@joachim-breitner.de mailto:mail@joachim-breitner.de>> wrote: > > Hi, > > Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack: > > I recommend acceptance. > > authored by Richard and Simon, and double-checked by Arnaud, I’m > happy > to concur. > > Cheers, > Joachim

-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 27 Old Gloucester Street, London WC1N 3AX, England

Arnaud Spiwack

10:47 a.m.

New subject: #547: Remove kind constraints, Recommendation: accept

Ok, then. I think that we can mark this proposal as accepted. On Fri, 25 Nov 2022 at 09:58, Adam Gundry wrote:

...

On 24/11/2022 09:22, Arnaud Spiwack wrote:

...
Adam makes an excellent point. GADTs defined with explicit equality constraints and then promoted is likely to be the main reason for breakage. If only because programmers doing that would probably not even really be aware that they are using constraints in kinds. On the other hand, I don't think that it's super common to defined a GADT that way, so the number of promoted GADTs will be small.

Adam, do you nevertheless support acceptance? Does anybody else have an opinion? I intend to mark the proposal as accepted tomorrow unless there is clear opposition.

Yes, I'm okay with acceptance. As you say, this is not the most common way to define GADTs, and given that (a) any class context prevents use in types, and (b) dependent pattern matching on GADTs doesn't work in type families anyway, it seems best to take the simple position that any context at all prevents use of a data constructor in a type.

Cheers,

Adam

...
On Tue, 22 Nov 2022 at 10:32, Adam Gundry mailto:adam@well-typed.com> wrote:

I'm not extremely worried about removing equality constraints in kinds themselves, but I am slightly worried that this proposal will unexpectedly prevent (existing) uses of GADTs with DataKinds. If I understand correctly, this version of MkT will be usable in types:

data T a where MkT :: Bool -> T Bool

but this will not (even though it could be rewritten to the former):

data T a where MkT :: a ~ Bool => Bool -> T a

Moreover, this MkT not be usable in types at all:

type family F a data T a where MkT :: F a ~ Bool => Bool -> T a

I suppose we can live with this in exchange for the gain in simplicity, especially as there seems to be agreement that maintaining the feature is simply too costly. But I would not be all that surprised if some users' code breaks as a result.

Cheers,

Adam

On 21/11/2022 08:32, Arnaud Spiwack wrote: > Not many opined. Unless there is opposition, I'll mark the proposal as > acceptable sometime before the end of the week. > > On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack mailto:arnaud.spiwack@tweag.io > mailto:arnaud.spiwack@tweag.io>> wrote: > > > authored by Richard and Simon, and double-checked by Arnaud, I’m > happy > > to concur. > > 😀 > > To clarify: the main question is whether we are confident that it > won't break too many users. I don't have divination powers that make > my word particularly trustworthy on this point. Yet, I do feel > pretty confident. > > On Mon, 14 Nov 2022 at 12:51, Joachim Breitner > mailto:mail@joachim-breitner.de mailto:mail@joachim-breitner.de>> wrote: > > Hi, > > Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack: > > I recommend acceptance. > > authored by Richard and Simon, and double-checked by Arnaud, I’m > happy > to concur. > > Cheers, > Joachim

-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890 27 Old Gloucester Street, London WC1N 3AX, England

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

907

Age (days ago)

918

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Adam Gundry
Arnaud Spiwack
Joachim Breitner

#547: Remove kind constraints, Recommendation: accept

tags

participants (3)