#536: Type-level literals as a separate language extension, rec: accept
Dear Committee, Ross Paterson has proposed #536 "Type-level literals as a separate language extension". Read it here: https://github.com/RossPaterson/ghc-proposals/blob/literals/proposals/0000-t... Currently the DataKinds extension allows us to use both type-level literals (such as "hello", 'x', and 42) and promoted algebraic data constructors (such as True, Just, and '[]). The proposal is to factor out promotion of literals into its own extension, TypeLevelLiterals. Why would one want to enable TypeLevelLiterals but not DataKinds? Because the latter can create ambiguities when it comes to name resolution. If the user defines `data Just x = ...` and they have DataKinds enabled, then suddenly it's ambiguous whether `Just` refers to a data constructor or a type constructor, and GHC starts to guess from context. Type-level literals, on the other hand, are a more conservative subset of DataKinds that does not raise any questions with regards to name resolution. While I, personally, would not use this conservative subset, I believe we shouldn't create obstacles for those who want to. I expect the maintenance costs to be minimal. Does anyone have objections? If not, I will mark the proposal accepted in 2 weeks. - Vlad
I'm content to accept this one. Simon On Mon, 6 Mar 2023 at 13:05, Vladislav Zavialov <vlad.z.4096@gmail.com> wrote:
Dear Committee,
Ross Paterson has proposed #536 "Type-level literals as a separate language extension". Read it here:
https://github.com/RossPaterson/ghc-proposals/blob/literals/proposals/0000-t...
Currently the DataKinds extension allows us to use both type-level literals (such as "hello", 'x', and 42) and promoted algebraic data constructors (such as True, Just, and '[]). The proposal is to factor out promotion of literals into its own extension, TypeLevelLiterals.
Why would one want to enable TypeLevelLiterals but not DataKinds? Because the latter can create ambiguities when it comes to name resolution. If the user defines `data Just x = ...` and they have DataKinds enabled, then suddenly it's ambiguous whether `Just` refers to a data constructor or a type constructor, and GHC starts to guess from context. Type-level literals, on the other hand, are a more conservative subset of DataKinds that does not raise any questions with regards to name resolution.
While I, personally, would not use this conservative subset, I believe we shouldn't create obstacles for those who want to. I expect the maintenance costs to be minimal.
Does anyone have objections? If not, I will mark the proposal accepted in 2 weeks.
- Vlad _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
Hi, Am Montag, dem 06.03.2023 um 16:04 +0300 schrieb Vladislav Zavialov:
Does anyone have objections? If not, I will mark the proposal accepted in 2 weeks.
not a full fledged objection yet, but I am unsure how that fits with the overall direction we have for namespaces, as outlined in https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-de... It this meant to be a short-gap measure that helps us to get to towards a bolder destination? Or is it a half-way step for people who like type-level computation, but don’t want to go all the way, and is expected to stay around? (Or maybe I am missing the point.) Unless I am missing the point, I can’t really make an informed decision before we have concluded our policy discussion, in particular, on whether we want to go towards a future where everyone is welcome to turn extensions on and off to build their little fine-grained preferred language islands, or whether that is something we want to avoid and use extensions only as stepping stones towards a ((eventually) single) future Haskell, at the cost of having to tell some people that they can’t expect that every possible dialect of Haskell will be supported. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
Unless I am missing the point, I can’t really make an informed decision before we have concluded our policy discussion, in particular, on whether we want to go towards a future where everyone is welcome to turn extensions on and off to build their little fine-grained preferred language islands, or whether that is something we want to avoid and use extensions only as stepping stones towards a ((eventually) single) future Haskell, at the cost of having to tell some people that they can’t expect that every possible dialect of Haskell will be supported.
I don't think these two are incompatible. Even if we have a "single future Haskell" in mind, it's fair enough for people to switch things on and off if they want. Offering flexiblity at low cost seems OK to me; other things being equal, it's not for us to say what they should or should not want. (If the implementation or maintenance cost was high I might think again, but I don't think it is in this case.) Simon On Mon, 6 Mar 2023 at 16:58, Joachim Breitner <mail@joachim-breitner.de> wrote:
Hi,
Am Montag, dem 06.03.2023 um 16:04 +0300 schrieb Vladislav Zavialov:
Does anyone have objections? If not, I will mark the proposal accepted in 2 weeks.
not a full fledged objection yet, but I am unsure how that fits with the overall direction we have for namespaces, as outlined in
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-de...
It this meant to be a short-gap measure that helps us to get to towards a bolder destination?
Or is it a half-way step for people who like type-level computation, but don’t want to go all the way, and is expected to stay around?
(Or maybe I am missing the point.)
Unless I am missing the point, I can’t really make an informed decision before we have concluded our policy discussion, in particular, on whether we want to go towards a future where everyone is welcome to turn extensions on and off to build their little fine-grained preferred language islands, or whether that is something we want to avoid and use extensions only as stepping stones towards a ((eventually) single) future Haskell, at the cost of having to tell some people that they can’t expect that every possible dialect of Haskell will be supported.
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
Hello, Am Mittwoch, dem 08.03.2023 um 10:57 +0000 schrieb Simon Peyton Jones:
Unless I am missing the point, I can’t really make an informed decision before we have concluded our policy discussion, in particular, on whether we want to go towards a future where everyone is welcome to turn extensions on and off to build their little fine-grained preferred language islands, or whether that is something we want to avoid and use extensions only as stepping stones towards a ((eventually) single) future Haskell, at the cost of having to tell some people that they can’t expect that every possible dialect of Haskell will be supported.
I don't think these two are incompatible. Even if we have a "single future Haskell" in mind, it's fair enough for people to switch things on and off if they want. Offering flexiblity at low cost seems OK to me; other things being equal, it's not for us to say what they should or should not want. (If the implementation or maintenance cost was high I might think again, but I don't think it is in this case.)
It is certainly a reasonable policy that we _want_ GHC Haskell to be highly customizable, and that users should be able to use language extensions to tailor the language to their needs and preferences. (So maybe we’d add UnqualifiedImports so that PVP-adherence can be enforced with -XNoUnqualifiedImports, and we’d add ASCIISyntax, so that fans of unicode can add -XNoASCIISyntax and get to use `forall` and `->` as variable names, since ∀ and → are the keywords now… – just building up a little strawmany army here…) But its also reasonable to say that, as convenient as it is for the individual developer asking for the feature, it’s not actualy good for the ecosystem as a whole. And this is not just about the implementation cost: It’s the cost of yet another language extension that people dealing with more than just their own code have to understand, to decide whether they want to use it, to worry about whether it’s on or off when reading code and (in this case) mentally resolving name. Choice is good for those who want the alternative, but incurs a (small, but relevant) cost on everyone! I see appeal in either policy, but they do seem rather incompatible to me, and I hope the general policy discussion will give us better guidelines here. More concretely about this proposal: It seems that one motivation is that DataKinds is “bad” in some way, namely in that term constructors are available in types. So if we accept this proposal, does that mean we agree with that assessment, what are we going to do about it? Is there a better way of referring to term constructors that we could work to wards to that works for everyone? Or are we going to have multiple future Haskell dialects, one with strict separation between terms and types, one with some things also on the type level (basic literals, but no tuples or user-defined constructors), and a third one that’s the full story? Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
On Wed, Mar 8, 2023 at 2:19 PM Joachim Breitner <mail@joachim-breitner.de> wrote:
It seems that one motivation is that DataKinds is “bad” in some way, namely in that term constructors are available in types. So if we accept this proposal, does that mean we agree with that assessment, what are we going to do about it? Is there a better way of referring to term constructors that we could work to wards to that works for everyone? Or are we going to have multiple future Haskell dialects, one with strict separation between terms and types, one with some things also on the type level (basic literals, but no tuples or user-defined constructors), and a third one that’s the full story?
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution. There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names. Each approach could indeed lead to a "dialect" of sorts. * The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type-level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378. If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept. - Vlad
Hi, Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context. Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee). On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de> wrote:
Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
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
Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. Richard
On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io> wrote:
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).
On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote: Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
Cheers, Joachim
-- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org <mailto:ghc-steering-committee@haskell.org> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <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
This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like. For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation. If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?). A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds. Adam On 09/03/2023 16:21, Richard Eisenberg wrote:
Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here.
Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.)
Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha).
Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub.
Richard
On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>> wrote:
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).
On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote:
Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov: > DataKinds is indeed a "bad" extension because it introduces ambiguity > to name resolution. > > There are two ways to avoid this issue: > 1. Keep namespaces separate and double down on using punned > constructor names. > 2. Merge terms and types, discouraging punned constructor names. > > Each approach could indeed lead to a "dialect" of sorts. > > * The (accepted and recently implemented) TypeData extension moves us > in the direction of option (1), and I imagine the proposed > TypeLevelLiterals would be often used in conjunction with TypeData. > This carves out a limited, conservative language subset for type- > level programming. > * At the same time, #270 "Support pun-free code" moves us in the > direction of option (2), and I expect it to be the better option when > it comes to fully fledged dependently-typed programming envisioned by > #378. > > If I had to choose, I'd go with option (2). I don't see myself using > TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a > thousand flowers bloom" persuasion, hence my recommendation to > accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
Cheers, Joachim
-- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
-- 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
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure. Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal. Richard
On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com> wrote:
This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like.
For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation.
If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?).
A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds.
Adam
On 09/03/2023 16:21, Richard Eisenberg wrote:
Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. Richard
On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>> wrote:
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).
On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote:
Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
Cheers, Joachim
-- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
-- 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
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want. On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not. This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote. Simon On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com> wrote:
This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like.
For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation.
If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?).
A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds.
Adam
On 09/03/2023 16:21, Richard Eisenberg wrote:
Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. Richard
On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>> wrote:
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).
On Wed, 8 Mar 2023 at 13:56, Joachim Breitner < mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote:
Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
Cheers, Joachim
-- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
-- 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
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
I am also in favour of extensions that focus on solving a single problem well and giving users precise control over what extensions they deploy. If we get this right then we should be able discover which extensions people want and those that are free of unintended consequences, and can put them on track to be included in a GHC and then Haskell standard. This proposal isn't ambitious but it does otherwise appear to qualify so I am in favour. Chris
On 20 Mar 2023, at 08:43, Simon Peyton Jones <simon.peytonjones@gmail.com> wrote:
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want.
On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not.
This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev <mailto:lists@richarde.dev>> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com <mailto:adam@well-typed.com>> wrote:
This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like.
For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation.
If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?).
A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds.
Adam
On 09/03/2023 16:21, Richard Eisenberg wrote:
Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. Richard
On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>>> wrote:
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).
On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>>> wrote:
Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
Cheers, Joachim
-- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
-- 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 <mailto: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 <mailto: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
Hello, I am not on the committee but as the original author of the type literals extensions I thought I'd give my 2c. I am strongly in favor of separating type literals from DataKinds, they are not really together for any deep reason. For me the separate extension would be useful because it makes it possible to use type literals with the `TypeData` extension, which for me, is a much nicer way to work with type level things than `DataKinds`. -Iavor On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <chris@chrisdornan.com> wrote:
I am also in favour of extensions that focus on solving a single problem well and giving users precise control over what extensions they deploy. If we get this right then we should be able discover which extensions people want and those that are free of unintended consequences, and can put them on track to be included in a GHC and then Haskell standard.
This proposal isn't ambitious but it does otherwise appear to qualify so I am in favour.
Chris
On 20 Mar 2023, at 08:43, Simon Peyton Jones <simon.peytonjones@gmail.com> wrote:
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want.
On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not.
This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com> wrote:
This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like.
For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation.
If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?).
A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds.
Adam
On 09/03/2023 16:21, Richard Eisenberg wrote:
Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. Richard
On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>> wrote:
I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee).
On Wed, 8 Mar 2023 at 13:56, Joachim Breitner < mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote:
Hi,
Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov:
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue: 1. Keep namespaces separate and double down on using punned constructor names. 2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type- level programming. * At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
Thanks for putting this into a clearer context.
Where does DataKind fit in? Is it a natural part of approach (2) (which is the general direction outlined by #378), or is yet another take on the issue? If DataKinds was not what we want according to #378, but the fragment carved out by TypeLevelLiterals was, then that would be a strong reason for me to acccept TypeLevelLiterals. But if DataKinds is the goal (or at least “the” goal), then I think I’d like to see stronger arguments for why it should be split.
Cheers, Joachim
-- Joachim Breitner mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
-- 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
_______________________________________________ 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
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
Thanks for your comments Iavor, your input is appreciated. The ongoing discussion on language extensions made me think about proposal #536 again. With due respect to Richard, I still think we should accept it, for the following reasons: * We owe it to proposal authors to make decisions in a reasonably prompt fashion. The ongoing discussion is unlikely to be resolved extremely quickly, and the extension split in the proposal accords with the de facto approach to language extensions as feature flags. * Even if we accept the premise that we have too many extensions, accepting the proposal doesn't really make things worse (if we already have a hundred extensions too many, what harm one more?). * As Iavor says, there is no deep reason for type literals and DataKinds to be grouped as part of the same feature; it is merely a historical accident. If we later move to a model where features are enabled by default and controlled using warnings, it would be equally reasonable to have separate warnings for type literals and DataKinds. * The proposed change is simple, low effort to implement and maintain, and is clearly desired by some users. * The workaround with -Werror=unticked-promoted-constructors doesn't accurately characterise the language with type literals but not DataKinds. Feel free to object, of course. :-) Adam On 20/03/2023 17:59, Iavor Diatchki wrote:
Hello,
I am not on the committee but as the original author of the type literals extensions I thought I'd give my 2c. I am strongly in favor of separating type literals from DataKinds, they are not really together for any deep reason.
For me the separate extension would be useful because it makes it possible to use type literals with the `TypeData` extension, which for me, is a much nicer way to work with type level things than `DataKinds`.
-Iavor
On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <chris@chrisdornan.com <mailto:chris@chrisdornan.com>> wrote:
I am also in favour of extensions that focus on solving a single problem well and giving users precise control over what extensions they deploy. If we get this right then we should be able discover which extensions people want and those that are free of unintended consequences, and can put them on track to be included in a GHC and then Haskell standard.
This proposal isn't ambitious but it does otherwise appear to qualify so I am in favour.
Chris
On 20 Mar 2023, at 08:43, Simon Peyton Jones <simon.peytonjones@gmail.com <mailto:simon.peytonjones@gmail.com>> wrote:
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want.
On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not.
This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev <mailto:lists@richarde.dev>> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
> On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com <mailto:adam@well-typed.com>> wrote: > > This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like. > > For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation. > > If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?). > > A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds. > > Adam > > > On 09/03/2023 16:21, Richard Eisenberg wrote: >> Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. >> Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) >> Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). >> Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. >> Richard >>> On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>>> wrote: >>> >>> I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee). >>> >>> On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>>> wrote: >>> >>> Hi, >>> >>> Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov: >>> > DataKinds is indeed a "bad" extension because it introduces >>> ambiguity >>> > to name resolution. >>> > >>> > There are two ways to avoid this issue: >>> > 1. Keep namespaces separate and double down on using punned >>> > constructor names. >>> > 2. Merge terms and types, discouraging punned constructor names. >>> > >>> > Each approach could indeed lead to a "dialect" of sorts. >>> > >>> > * The (accepted and recently implemented) TypeData extension >>> moves us >>> > in the direction of option (1), and I imagine the proposed >>> > TypeLevelLiterals would be often used in conjunction with TypeData. >>> > This carves out a limited, conservative language subset for type- >>> > level programming. >>> > * At the same time, #270 "Support pun-free code" moves us in the >>> > direction of option (2), and I expect it to be the better option >>> when >>> > it comes to fully fledged dependently-typed programming >>> envisioned by >>> > #378. >>> > >>> > If I had to choose, I'd go with option (2). I don't see myself using >>> > TypeData, nor TypeLevelLiterals for that matter. But I am of a >>> "let a >>> > thousand flowers bloom" persuasion, hence my recommendation to >>> > accept. >>> >>> >>> Thanks for putting this into a clearer context. >>> >>> Where does DataKind fit in? Is it a natural part of approach (2) >>> (which >>> is the general direction outlined by #378), or is yet another take on >>> the issue? >>> If DataKinds was not what we want according to #378, but the fragment >>> carved out by TypeLevelLiterals was, then that would be a strong >>> reason >>> for me to acccept TypeLevelLiterals. >>> But if DataKinds is the goal (or at least “the” goal), then I >>> think I’d >>> like to see stronger arguments for why it should be split. >>> >>> >>> 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
I am also in favour for the reasons Adam gives. Simon On Mon, 1 May 2023 at 14:17, Adam Gundry <adam@well-typed.com> wrote:
Thanks for your comments Iavor, your input is appreciated.
The ongoing discussion on language extensions made me think about proposal #536 again. With due respect to Richard, I still think we should accept it, for the following reasons:
* We owe it to proposal authors to make decisions in a reasonably prompt fashion. The ongoing discussion is unlikely to be resolved extremely quickly, and the extension split in the proposal accords with the de facto approach to language extensions as feature flags.
* Even if we accept the premise that we have too many extensions, accepting the proposal doesn't really make things worse (if we already have a hundred extensions too many, what harm one more?).
* As Iavor says, there is no deep reason for type literals and DataKinds to be grouped as part of the same feature; it is merely a historical accident. If we later move to a model where features are enabled by default and controlled using warnings, it would be equally reasonable to have separate warnings for type literals and DataKinds.
* The proposed change is simple, low effort to implement and maintain, and is clearly desired by some users.
* The workaround with -Werror=unticked-promoted-constructors doesn't accurately characterise the language with type literals but not DataKinds.
Feel free to object, of course. :-)
Adam
On 20/03/2023 17:59, Iavor Diatchki wrote:
Hello,
I am not on the committee but as the original author of the type literals extensions I thought I'd give my 2c. I am strongly in favor of separating type literals from DataKinds, they are not really together for any deep reason.
For me the separate extension would be useful because it makes it possible to use type literals with the `TypeData` extension, which for me, is a much nicer way to work with type level things than `DataKinds`.
-Iavor
On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <chris@chrisdornan.com <mailto:chris@chrisdornan.com>> wrote:
I am also in favour of extensions that focus on solving a single problem well and giving users precise control over what extensions they deploy. If we get this right then we should be able discover which extensions people want and those that are free of unintended consequences, and can put them on track to be included in a GHC and then Haskell standard.
This proposal isn't ambitious but it does otherwise appear to qualify so I am in favour.
Chris
On 20 Mar 2023, at 08:43, Simon Peyton Jones <simon.peytonjones@gmail.com <mailto:simon.peytonjones@gmail.com>> wrote:
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want.
On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not.
This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev <mailto:lists@richarde.dev>> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
> On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com <mailto:adam@well-typed.com>> wrote: > > This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like. > > For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation. > > If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?). > > A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds. > > Adam > > > On 09/03/2023 16:21, Richard Eisenberg wrote: >> Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. >> Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) >> Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). >> Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. >> Richard >>> On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>>> wrote: >>> >>> I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee). >>> >>> On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>>> wrote: >>> >>> Hi, >>> >>> Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov: >>> > DataKinds is indeed a "bad" extension because it introduces >>> ambiguity >>> > to name resolution. >>> > >>> > There are two ways to avoid this issue: >>> > 1. Keep namespaces separate and double down on using punned >>> > constructor names. >>> > 2. Merge terms and types, discouraging punned constructor names. >>> > >>> > Each approach could indeed lead to a "dialect" of
sorts.
>>> > >>> > * The (accepted and recently implemented) TypeData extension >>> moves us >>> > in the direction of option (1), and I imagine the proposed >>> > TypeLevelLiterals would be often used in conjunction with TypeData. >>> > This carves out a limited, conservative language subset for type- >>> > level programming. >>> > * At the same time, #270 "Support pun-free code" moves us in the >>> > direction of option (2), and I expect it to be the better option >>> when >>> > it comes to fully fledged dependently-typed programming >>> envisioned by >>> > #378. >>> > >>> > If I had to choose, I'd go with option (2). I don't see myself using >>> > TypeData, nor TypeLevelLiterals for that matter. But I am of a >>> "let a >>> > thousand flowers bloom" persuasion, hence my recommendation to >>> > accept. >>> >>> >>> Thanks for putting this into a clearer context. >>> >>> Where does DataKind fit in? Is it a natural part of approach (2) >>> (which >>> is the general direction outlined by #378), or is yet another take on >>> the issue? >>> If DataKinds was not what we want according to #378, but the fragment >>> carved out by TypeLevelLiterals was, then that would be a strong >>> reason >>> for me to acccept TypeLevelLiterals. >>> But if DataKinds is the goal (or at least “the” goal), then I >>> think I’d >>> like to see stronger arguments for why it should be
split.
>>> >>> >>> 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
I remain opposed, but I understand that I'm in the minority here. Richard
On May 1, 2023, at 2:19 PM, Simon Peyton Jones <simon.peytonjones@gmail.com> wrote:
I am also in favour for the reasons Adam gives.
Simon
On Mon, 1 May 2023 at 14:17, Adam Gundry <adam@well-typed.com <mailto:adam@well-typed.com>> wrote: Thanks for your comments Iavor, your input is appreciated.
The ongoing discussion on language extensions made me think about proposal #536 again. With due respect to Richard, I still think we should accept it, for the following reasons:
* We owe it to proposal authors to make decisions in a reasonably prompt fashion. The ongoing discussion is unlikely to be resolved extremely quickly, and the extension split in the proposal accords with the de facto approach to language extensions as feature flags.
* Even if we accept the premise that we have too many extensions, accepting the proposal doesn't really make things worse (if we already have a hundred extensions too many, what harm one more?).
* As Iavor says, there is no deep reason for type literals and DataKinds to be grouped as part of the same feature; it is merely a historical accident. If we later move to a model where features are enabled by default and controlled using warnings, it would be equally reasonable to have separate warnings for type literals and DataKinds.
* The proposed change is simple, low effort to implement and maintain, and is clearly desired by some users.
* The workaround with -Werror=unticked-promoted-constructors doesn't accurately characterise the language with type literals but not DataKinds.
Feel free to object, of course. :-)
Adam
On 20/03/2023 17:59, Iavor Diatchki wrote:
Hello,
I am not on the committee but as the original author of the type literals extensions I thought I'd give my 2c. I am strongly in favor of separating type literals from DataKinds, they are not really together for any deep reason.
For me the separate extension would be useful because it makes it possible to use type literals with the `TypeData` extension, which for me, is a much nicer way to work with type level things than `DataKinds`.
-Iavor
On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <chris@chrisdornan.com <mailto:chris@chrisdornan.com> <mailto:chris@chrisdornan.com <mailto:chris@chrisdornan.com>>> wrote:
I am also in favour of extensions that focus on solving a single problem well and giving users precise control over what extensions they deploy. If we get this right then we should be able discover which extensions people want and those that are free of unintended consequences, and can put them on track to be included in a GHC and then Haskell standard.
This proposal isn't ambitious but it does otherwise appear to qualify so I am in favour.
Chris
On 20 Mar 2023, at 08:43, Simon Peyton Jones <simon.peytonjones@gmail.com <mailto:simon.peytonjones@gmail.com> <mailto:simon.peytonjones@gmail.com <mailto:simon.peytonjones@gmail.com>>> wrote:
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want.
On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not.
This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev <mailto:lists@richarde.dev> <mailto:lists@richarde.dev <mailto:lists@richarde.dev>>> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
> On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com <mailto:adam@well-typed.com> <mailto:adam@well-typed.com <mailto:adam@well-typed.com>>> wrote: > > This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like. > > For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation. > > If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?). > > A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds. > > Adam > > > On 09/03/2023 16:21, Richard Eisenberg wrote: >> Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. >> Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) >> Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals -XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). >> Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. >> Richard >>> On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>>>> wrote: >>> >>> I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee). >>> >>> On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>>>> wrote: >>> >>> Hi, >>> >>> Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov: >>> > DataKinds is indeed a "bad" extension because it introduces >>> ambiguity >>> > to name resolution. >>> > >>> > There are two ways to avoid this issue: >>> > 1. Keep namespaces separate and double down on using punned >>> > constructor names. >>> > 2. Merge terms and types, discouraging punned constructor names. >>> > >>> > Each approach could indeed lead to a "dialect" of sorts. >>> > >>> > * The (accepted and recently implemented) TypeData extension >>> moves us >>> > in the direction of option (1), and I imagine the proposed >>> > TypeLevelLiterals would be often used in conjunction with TypeData. >>> > This carves out a limited, conservative language subset for type- >>> > level programming. >>> > * At the same time, #270 "Support pun-free code" moves us in the >>> > direction of option (2), and I expect it to be the better option >>> when >>> > it comes to fully fledged dependently-typed programming >>> envisioned by >>> > #378. >>> > >>> > If I had to choose, I'd go with option (2). I don't see myself using >>> > TypeData, nor TypeLevelLiterals for that matter. But I am of a >>> "let a >>> > thousand flowers bloom" persuasion, hence my recommendation to >>> > accept. >>> >>> >>> Thanks for putting this into a clearer context. >>> >>> Where does DataKind fit in? Is it a natural part of approach (2) >>> (which >>> is the general direction outlined by #378), or is yet another take on >>> the issue? >>> If DataKinds was not what we want according to #378, but the fragment >>> carved out by TypeLevelLiterals was, then that would be a strong >>> reason >>> for me to acccept TypeLevelLiterals. >>> But if DataKinds is the goal (or at least “the” goal), then I >>> think I’d >>> like to see stronger arguments for why it should be split. >>> >>> >>> Cheers, >>> Joachim
-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ <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 <mailto:ghc-steering-committee@haskell.org> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <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
Hi, I am also part of that minority, but at least until and unless we come to a clear policy that we want to wean off fine-grined language pragmas, I don’t want to block the enthusiasm of those who have stronger opinions in favor of this particular one. As Adam says, we already have very many extensions, so YOLO. Cheers, Joachim Am Montag, dem 08.05.2023 um 11:48 +0000 schrieb Richard Eisenberg:
I remain opposed, but I understand that I'm in the minority here.
Richard
On May 1, 2023, at 2:19 PM, Simon Peyton Jones <simon.peytonjones@gmail.com> wrote:
I am also in favour for the reasons Adam gives.
Simon
On Mon, 1 May 2023 at 14:17, Adam Gundry <adam@well-typed.com> wrote:
Thanks for your comments Iavor, your input is appreciated.
The ongoing discussion on language extensions made me think about proposal #536 again. With due respect to Richard, I still think we should accept it, for the following reasons:
* We owe it to proposal authors to make decisions in a reasonably prompt fashion. The ongoing discussion is unlikely to be resolved extremely quickly, and the extension split in the proposal accords with the de facto approach to language extensions as feature flags.
* Even if we accept the premise that we have too many extensions, accepting the proposal doesn't really make things worse (if we already have a hundred extensions too many, what harm one more?).
* As Iavor says, there is no deep reason for type literals and DataKinds to be grouped as part of the same feature; it is merely a historical accident. If we later move to a model where features are enabled by default and controlled using warnings, it would be equally reasonable to have separate warnings for type literals and DataKinds.
* The proposed change is simple, low effort to implement and maintain, and is clearly desired by some users.
* The workaround with -Werror=unticked-promoted-constructors doesn't accurately characterise the language with type literals but not DataKinds.
Feel free to object, of course. :-)
Adam
On 20/03/2023 17:59, Iavor Diatchki wrote:
Hello,
I am not on the committee but as the original author of the type literals extensions I thought I'd give my 2c. I am strongly in favor of separating type literals from DataKinds, they are not really together for any deep reason.
For me the separate extension would be useful because it makes it possible to use type literals with the `TypeData` extension, which for me, is a much nicer way to work with type level things than `DataKinds`.
-Iavor
On Mon, Mar 20, 2023 at 10:08 AM Chris Dornan <chris@chrisdornan.com <mailto:chris@chrisdornan.com>> wrote:
I am also in favour of extensions that focus on solving a single problem well and giving users precise control over what extensions they deploy. If we get this right then we should be able discover which extensions people want and those that are free of unintended consequences, and can put them on track to be included in a GHC and then Haskell standard.
This proposal isn't ambitious but it does otherwise appear to qualify so I am in favour.
Chris
On 20 Mar 2023, at 08:43, Simon Peyton Jones <simon.peytonjones@gmail.com <mailto:simon.peytonjones@gmail.com>> wrote:
Personally I'm happy with having orthogonal extensions that enable just one thing. That allows our users to do what they want, rather than telling them what they want.
On this particular proposal I don't think it's a big deal either way, but I'd vote in favour. It's not exactly true to say that it duplicates an existing feature. I think Richard's point is that you can get a warning for using an unticked constructor (but nothing for using a ticked one). That's different from getting an error if you use a constructor in a type, ticked or not.
This particular proposal is easy to describe and easy to implement. But I don't think we should burn a lot of cycles on it... it's a matter of taste, so we could just vote.
Simon
On Sun, 19 Mar 2023 at 21:09, Richard Eisenberg <lists@richarde.dev <mailto:lists@richarde.dev>> wrote:
This argument gave me pause. Thanks, Adam. I think, for me, it comes down to this: what do we think will be more useful to more of our users? A notion of a core language -- perhaps implemented by different compilers -- with extensions? Or a unified language GHC/Haskell which allows subsetting? I tend to think the latter, though I'm not sure.
Regarding this particular proposal: I remain against the proposal, as it duplicates an existing feature. That's a simple reason to be against a proposal.
Richard
> On Mar 10, 2023, at 9:15 AM, Adam Gundry <adam@well-typed.com <mailto:adam@well-typed.com>> wrote: > > This proposal is very helpful in exposing some of the divisions about the interpretation of extensions that exist within the committee! "Let a thousand flowers bloom" vs "more-extensions-make-me-wince", if you like. > > For what it's worth I tend to be in the former camp. I think we should strive for orthogonality and avoid bundling together distinct features merely because they have related effects. Instead we should construct our language via composition of simple components. And I think it's reasonable to say that TypeLevelLiterals and (the rest of) DataKinds are clearly distinct and can be understood in isolation. > > If the number of extensions is a problem, that points to the need to better structure our documentation and gather coherent subsets of extensions into manageable pieces (much as GHC2021 tries to do). Beyond that I'd like to understand the downsides better (e.g. what costs does it actually impose on HLS to have another extension?). > > A conversation with one of the authors of Helium this week made me think that in the GHC proposals process we have tended to neglect the possible presence of other Haskell implementations. It's not realistic to expect that anyone will reimplement the whole of GHC Haskell, but perhaps there is a fragment large enough to be useful for a fair number of Haskell programs but also small enough to be independently implemented (e.g. by Helium). It would strike me as plausible that such an implementation might want to support TypeData+TypeLevelLiterals but not DataKinds. > > Adam > > > On 09/03/2023 16:21, Richard Eisenberg wrote: >> Though I see the arguments in the other direction, I vote against this proposal. As Joachim argues, adding an extension puts a tax on the entire ecosystem by adding one more bit of context a reader has to have to understand code. In addition, HLS will have to be aware of this extension. And the benefits seem pretty marginal here. >> Can we instead simply provide a warning? The warning here would be something like the -Wpuns idea, in that it helps the author keep to a particular subset of the language. (We might want to collect such warnings somehow in our documentation.) >> Actually, it occurs to me we already have the warning: -Wunticked-promoted-constructors. We've put that warning in the -Weverything bin (not even -Wall) because in the past we've decided that we shouldn't recommend/require the ' when using a constructor in a type. But actually, setting -Werror=unticked-promoted-constructors would seem to be a perfect substitute for -XTypeLevelLiterals - XNoDataKinds. OK, not perfect: you could still use a constructor in a type with a ' mark. But I think that's great, actually, because perhaps an author wary of constructors in types still might need to use one, in one place, in a 2,000-line file. This ticks all the boxes (ha ha). >> Having discovered this replacement, I'm now pretty strongly against this proposal. I'll also post on GitHub. >> Richard >>> On Mar 9, 2023, at 4:26 AM, Arnaud Spiwack <arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io> <mailto:arnaud.spiwack@tweag.io <mailto:arnaud.spiwack@tweag.io>>> wrote: >>> >>> I can see where the author is coming from. But as Joachim, I find myself unconvinced that it is worth yet one extra extension (but then again, I'm the more-extensions-make-me-wince member of this committee). >>> >>> On Wed, 8 Mar 2023 at 13:56, Joachim Breitner <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de> <mailto:mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>>> wrote: >>> >>> Hi, >>> >>> Am Mittwoch, dem 08.03.2023 um 14:58 +0300 schrieb Vladislav Zavialov: >>> > DataKinds is indeed a "bad" extension because it introduces >>> ambiguity >>> > to name resolution. >>> > >>> > There are two ways to avoid this issue: >>> > 1. Keep namespaces separate and double down on using punned >>> > constructor names. >>> > 2. Merge terms and types, discouraging punned constructor names. >>> > >>> > Each approach could indeed lead to a "dialect" of sorts. >>> > >>> > * The (accepted and recently implemented) TypeData extension >>> moves us >>> > in the direction of option (1), and I imagine the proposed >>> > TypeLevelLiterals would be often used in conjunction with TypeData. >>> > This carves out a limited, conservative language subset for type- >>> > level programming. >>> > * At the same time, #270 "Support pun-free code" moves us in the >>> > direction of option (2), and I expect it to be the better option >>> when >>> > it comes to fully fledged dependently-typed programming >>> envisioned by >>> > #378. >>> > >>> > If I had to choose, I'd go with option (2). I don't see myself using >>> > TypeData, nor TypeLevelLiterals for that matter. But I am of a >>> "let a >>> > thousand flowers bloom" persuasion, hence my recommendation to >>> > accept. >>> >>> >>> Thanks for putting this into a clearer context. >>> >>> Where does DataKind fit in? Is it a natural part of approach (2) >>> (which >>> is the general direction outlined by #378), or is yet another take on >>> the issue? >>> If DataKinds was not what we want according to #378, but the fragment >>> carved out by TypeLevelLiterals was, then that would be a strong >>> reason >>> for me to acccept TypeLevelLiterals. >>> But if DataKinds is the goal (or at least “the” goal), then I >>> think I’d >>> like to see stronger arguments for why it should be split. >>> >>> >>> 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
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
-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
participants (8)
-
Adam Gundry -
Arnaud Spiwack -
Chris Dornan -
Iavor Diatchki -
Joachim Breitner -
Richard Eisenberg -
Simon Peyton Jones -
Vladislav Zavialov