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
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).
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
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.orghttps://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee