[ghc-steering-committee] #536: Type-level literals as a separate language extension, rec: accept

[Richard Eisenberg]

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> 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>> 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 at joachim-breitner.de <mailto:mail at joachim-breitner.de>
>   http://www.joachim-breitner.de/ <http://www.joachim-breitner.de/>
> 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org <mailto:ghc-steering-committee at 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 at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230309/76fe9173/attachment.html>