#536: Type-level literals as a separate language extension

Vladislav Zavialov

18 Oct 2023 18 Oct '23

12:30 p.m.

Dear Committee, Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals. I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor" Haven't yet expressed their opinion: Simon M. and Moritz. So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps: 1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell) The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not? The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer? Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us. Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all) The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds If any of the above (or similar) applies, speak up. Vlad

Attachments:

attachment.html (text/html — 5.4 KB)

Show replies by date

Joachim Breitner

18 Oct 18 Oct

1:31 p.m.

New subject: #536: Type-level literals as a separate language extension

Hi, thanks for the well thought through message and helpful conceptualisation. I agree that it would be good if the Committee as a whole would commit to one or the other paradigm. Am Mittwoch, dem 18.10.2023 um 18:30 +0200 schrieb Vladislav Zavialov:

...

(Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

my understanding with splitting ScopedTypeVariables is not to let a thousands (or 2³ in this case) flowers bloom, but to slice it into the parts we want to keep and the parts we (or some of us) want to change. Maybe not absolutely necessary, as we could have -XTheNewWay with some overlapping functionality with ScopedTypeVariables, such as annotating patterns with their types, but maybe even if it only serves to help communicating the changes it maybe worth it. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Simon Marlow

19 Oct 19 Oct

3:06 a.m.

New subject: #536: Type-level literals as a separate language extension

Thanks for the helpful summary Vlad! Admittedly I hadn't grasped the nub of the issue until now. Regarding: Unfortunately, we don't have a general policy that would clearly tell us

...

which camp/paradigm is right.

I think we actually do have a policy that's relevant here, see "Does not create a language fork" in https://github.com/ghc-proposals/ghc-proposals#review-criteria This essentially says we are biased *against* the "customizable Haskell" position and in favour of the monotonically-increasing-set-of-language-features position. Cheers Simon On Wed, 18 Oct 2023 at 17:30, Vladislav Zavialov wrote:

...

Dear Committee,

Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals.

I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor"

Haven't yet expressed their opinion: Simon M. and Moritz.

So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps:

1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell)

The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not?

The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer?

Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us.

Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds

If any of the above (or similar) applies, speak up.

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

Arnaud Spiwack

3:25 a.m.

New subject: #536: Type-level literals as a separate language extension

I don't think that the non-forking principle informs completely on the debate at hand. Even if the extensions are monotonic increases on the current language, even if an extension will either be merged into the next GHC20xx or scrapped, the question of splitting an extension in two still has validity. You may say: well, what if we adopt the type-level literals without adopting data kinds? I must, at any rate, apologise: it's my role to get to a resolution on the question of extension policy. This is going slow, and I've paused the process during the recent discussion on stability (I'm currently at capacity for committee work). We definitely can't wait until the policy has been well-defined before we can make a decision on the proposal at hand. I said I was unconvinced the last time around. I haven't changed opinion, but I'm happy to revise if presented with a sufficiently strong motivation. On Thu, 19 Oct 2023 at 09:07, Simon Marlow wrote:

...

Thanks for the helpful summary Vlad! Admittedly I hadn't grasped the nub of the issue until now.

Regarding:

Unfortunately, we don't have a general policy that would clearly tell us

...
which camp/paradigm is right.

I think we actually do have a policy that's relevant here, see "Does not create a language fork" in https://github.com/ghc-proposals/ghc-proposals#review-criteria

This essentially says we are biased *against* the "customizable Haskell" position and in favour of the monotonically-increasing-set-of-language-features position.

Cheers Simon

On Wed, 18 Oct 2023 at 17:30, Vladislav Zavialov wrote:

...
Dear Committee,

Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals.

I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor"

Haven't yet expressed their opinion: Simon M. and Moritz.

So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps:

1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell)

The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not?

The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer?

Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us.

Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds

If any of the above (or similar) applies, speak up.

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

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

-- Arnaud Spiwack Director, Research at https://moduscreate.com and https://tweag.io.

Simon Marlow

20 Oct 20 Oct

10:57 a.m.

New subject: #536: Type-level literals as a separate language extension

Arnaud: yes you're right, I was commenting more on the alternate philosophies identified by Vlad rather than this particular proposal. As far as this proposal goes, I agree it's not a fork, and I don't have a strong opinion about it. Cheers Simon On Thu, 19 Oct 2023 at 08:26, Arnaud Spiwack wrote:

...

I don't think that the non-forking principle informs completely on the debate at hand. Even if the extensions are monotonic increases on the current language, even if an extension will either be merged into the next GHC20xx or scrapped, the question of splitting an extension in two still has validity. You may say: well, what if we adopt the type-level literals without adopting data kinds?

I must, at any rate, apologise: it's my role to get to a resolution on the question of extension policy. This is going slow, and I've paused the process during the recent discussion on stability (I'm currently at capacity for committee work). We definitely can't wait until the policy has been well-defined before we can make a decision on the proposal at hand.

I said I was unconvinced the last time around. I haven't changed opinion, but I'm happy to revise if presented with a sufficiently strong motivation.

On Thu, 19 Oct 2023 at 09:07, Simon Marlow wrote:

...
Thanks for the helpful summary Vlad! Admittedly I hadn't grasped the nub of the issue until now.

Regarding:

Unfortunately, we don't have a general policy that would clearly tell us

...
which camp/paradigm is right.

I think we actually do have a policy that's relevant here, see "Does not create a language fork" in https://github.com/ghc-proposals/ghc-proposals#review-criteria

This essentially says we are biased *against* the "customizable Haskell" position and in favour of the monotonically-increasing-set-of-language-features position.

Cheers Simon

On Wed, 18 Oct 2023 at 17:30, Vladislav Zavialov wrote:

...
Dear Committee,

Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals.

I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor"

Haven't yet expressed their opinion: Simon M. and Moritz.

So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps:

1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell)

The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not?

The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer?

Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us.

Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds

If any of the above (or similar) applies, speak up.

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

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

-- Arnaud Spiwack Director, Research at https://moduscreate.com and https://tweag.io.

Simon Peyton Jones

19 Oct 19 Oct

1:32 p.m.

New subject: #536: Type-level literals as a separate language extension

I (now) lean to rejection, but not strongly so. I have expressed my view on the discussion https://github.com/ghc-proposals/ghc-proposals/pull/536#issuecomment-1771422... Simon On Wed, 18 Oct 2023 at 18:30, Vladislav Zavialov wrote:

...

Dear Committee,

Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals.

I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor"

Haven't yet expressed their opinion: Simon M. and Moritz.

So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps:

1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell)

The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not?

The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer?

Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us.

Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds

If any of the above (or similar) applies, speak up.

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

Adam Gundry

20 Oct 20 Oct

7:16 a.m.

New subject: #536: Type-level literals as a separate language extension

I remain in favour of this proposal. I think minimizing the *number* of extensions is fundamentally the wrong approach; instead we should aim to minimize *complexity*, both of individual extensions and of the system as a whole. It seems to me that this proposal makes DataKinds less complex, by decomposing it into simpler independent pieces. Indeed, as Simon mentions on the PR thread, we could reasonably give names to both these pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion. Cheers, Adam On 18/10/2023 17:30, Vladislav Zavialov wrote:

...

Dear Committee,

Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals.

I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor"

Haven't yet expressed their opinion: Simon M. and Moritz.

So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps:

1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell)

The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not?

The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer?

Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us.

Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds

If any of the above (or similar) applies, speak up.

Vlad

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org 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

Simon Peyton Jones

7:45 a.m.

New subject: #536: Type-level literals as a separate language extension

...

It seems to me that this proposal makes DataKinds less complex, by decomposing it into simpler independent pieces. Indeed, as Simon mentions on the PR thread, we could reasonably give names to both these pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion

If we accept at all, I would strongly like to accept in this form. Simon On Fri, 20 Oct 2023 at 12:16, Adam Gundry wrote:

...

I remain in favour of this proposal. I think minimizing the *number* of extensions is fundamentally the wrong approach; instead we should aim to minimize *complexity*, both of individual extensions and of the system as a whole.

It seems to me that this proposal makes DataKinds less complex, by decomposing it into simpler independent pieces. Indeed, as Simon mentions on the PR thread, we could reasonably give names to both these pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion.

Cheers,

Adam

On 18/10/2023 17:30, Vladislav Zavialov wrote:

...
Dear Committee,

Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals.

I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor"

Haven't yet expressed their opinion: Simon M. and Moritz.

So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps:

1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell)

The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not?

The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer?

Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us.

Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all)

The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds

If any of the above (or similar) applies, speak up.

Vlad

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org 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

Chris Dornan

11:55 a.m.

New subject: #536: Type-level literals as a separate language extension

I agree -- inherent complexity is the issue and this proposal helps with that. +1 from me. Chris

...

On 20 Oct 2023, at 12:16, Adam Gundry wrote:

I remain in favour of this proposal. I think minimizing the *number* of extensions is fundamentally the wrong approach; instead we should aim to minimize *complexity*, both of individual extensions and of the system as a whole.

It seems to me that this proposal makes DataKinds less complex, by decomposing it into simpler independent pieces. Indeed, as Simon mentions on the PR thread, we could reasonably give names to both these pieces so that DataKinds = TypeLevelLiterals + DataTypePromotion.

Cheers,

Adam

On 18/10/2023 17:30, Vladislav Zavialov wrote:

...
Dear Committee, Back in March I initiated a discussion of #536 "Type-level literals as a separate language extension" by Ross Paterson. Quick recap: currently DataKinds controls promotion of ADTs and Symbol/Natural/Char literals. The proposal is to factor out promotion of literals into their own extension, TypeLevelLiterals. I recommended acceptance but received mixed feedback. Summary of opinions: Vlad: "rec: accept" SPJ: "content to accept" Joachim: "unsure how that fits with the overall direction we have for namespaces" Arnaud: "unconvinced that it is worth yet one extra extension" Richard: "pretty strongly against" Adam: "avoid bundling together distinct features" (i.e. accept) Chris: "in favour" Iavor (as ex-member): "strongly in favor" Haven't yet expressed their opinion: Simon M. and Moritz. So we have roughly 5 votes in-favor-or-don't-mind and 3 votes against-or-unconvinced. SPJ suggested that we simply count the votes, but after reading the discussion, I find that there's a deeper reason for disagreement. Essentially, we have two camps: 1. "Let a thousand flowers bloom": Haskell should be customizable, built out of small extensions à la carte. (A necessary implication here is that this gives rise to dialects of Haskell that depend on the set of enabled extensions) 2. "More extensions make me wince": Extensions are a necessary evil while we explore the language design space, and we shouldn't create them unnecessarily. (Language editions like GHC2021 help with that, allowing the users to forget about individual extensions and simply use a better/newer Haskell) The 1st paradigm suggests that TypeLevelLiterals should be factored out. TypeLevelLiterals+TypeData form a dialect different from DataKinds with regards to name resolution, which some users might prefer. Let them have it, why not? The 2nd paradigm suggests that breaking DataKinds into smaller extensions is counterproductive. Do we want fewer extensions or more extensions, after all? And as a steering committee, don't we have a clear direction in which we steer? Unfortunately, we don't have a general policy that would clearly tell us which camp/paradigm is right. And it's about time that we make a decision regarding #536, even if we don't have a policy to guide us. Because of that, my new plan is to reject the proposal out of caution. We have at least one "strongly against", and it's enough to give me pause. It's probably better to stick to the status quo, at least until we develop a concrete stance w.r.t. fine-grained extensions. (Pardon a digression, but this also calls into question whether 448 is justified in splitting ScopedTypeVariables into ExtendedForAllScope, MethodTypeVariables, PatternSignatures. Maybe we don't want fine-grained extensions after all) The new recommendation is to reject the proposal, but I still can't make this decision single-handedly. So let's do another round of discussion, only this time let's stick to practicalities, not general considerations. Is there anyone on the committee (or do we know someone) who needs TypeLevelLiterals for practical reasons, not just as a matter of taste? For example, 1. You are writing a book and you want to introduce TypeLevelLiterals before DataKinds 2. You are developing or maintaining a library or application that needs TypeLevelLiterals but cannot use DataKinds 3. You are working on an alternative Haskell implementation and intend to support TypeLevelLiterals but not DataKinds If any of the above (or similar) applies, speak up. Vlad _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org 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

578

Age (days ago)

580

Last active (days ago)

List overview

Download

8 comments

7 participants

participants (7)

Adam Gundry
Arnaud Spiwack
Chris Dornan
Joachim Breitner
Simon Marlow
Simon Peyton Jones
Vladislav Zavialov

#536: Type-level literals as a separate language extension

tags

participants (7)