[ghc-steering-committee] #536: Type-level literals as a separate language extension, rec: accept
Joachim Breitner
mail at joachim-breitner.de
Tue May 9 12:57:01 UTC 2023
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 at 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 at 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 at chrisdornan.com
> > > > <mailto:chris at 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 at gmail.com
> > > > > <mailto:simon.peytonjones at 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 at richarde.dev <mailto:lists at 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 at well-typed.com <mailto:adam at 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 at tweag.io
> > > > > <mailto:arnaud.spiwack at tweag.io>
> > > > > <mailto:arnaud.spiwack at tweag.io
> > > > > <mailto:arnaud.spiwack at 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 at joachim-breitner.de
> > > > > <mailto:mail at joachim-breitner.de>
> > > > > <mailto:mail at joachim-breitner.de
> > > > > <mailto:mail at 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 at haskell.org
> > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
--
Joachim Breitner
mail at joachim-breitner.de
http://www.joachim-breitner.de/
More information about the ghc-steering-committee
mailing list