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
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