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

[Vladislav Zavialov]

On Wed, Mar 8, 2023 at 2:19 PM Joachim Breitner <mail at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230308/b2dee3ff/attachment-0001.html>