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

[Arnaud Spiwack]

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>
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
>   http://www.joachim-breitner.de/
>
> _______________________________________________
> 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/bb0bb74b/attachment.html>