#547: Remove kind constraints, Recommendation: accept
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
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/
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 <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
-- 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
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 <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 <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
-- 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
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 <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 <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 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
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 <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 <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 <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 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
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 <adam@well-typed.com <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 <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> > <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 > <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <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
Ok, then. I think that we can mark this proposal as accepted. On Fri, 25 Nov 2022 at 09:58, Adam Gundry <adam@well-typed.com> 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 <adam@well-typed.com <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 <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> > <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 > <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <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
participants (3)
-
Adam Gundry -
Arnaud Spiwack -
Joachim Breitner