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

[Joachim Breitner]

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/