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/