Re: [ghc-steering-committee] Please review "Visible 'forall' in types of terms" #281

Hi, Am Montag, den 23.11.2020, 18:22 +0000 schrieb Richard Eisenberg:

On Nov 23, 2020, at 3:10 AM, Joachim Breitner wrote:

...

My impression is that all (most?) of those working towards a Dependent Haskell world assume that we get a unified namespace with no punning

That indeed has been my assumption, but I've been reminded recently that this assumption is just that. In particular, combining types and terms is not strictly necessary to support dependent types. I do think it's necessary to have the smooth, happy dependent types I yearn for, but maybe we can't always get what we want. I don't want to distract this particular thread with the details (which would take some work to spell out), but I will admit that this merger is not strictly necessary for dependent types -- and perhaps the merger is precisely what I mean when I use "ergonomic" in #378.

Hmm, I think the emphasis above was lost in written communication, I meant “that we get a unified namespace _with no punning_”. What would a unified namespace with punning mean? It means there is no inherent difference between what is now a data constructor and a type constructor, i.e. a unified namespace, but set up so that juggling the fact that the same name may be used in multiple places is ergonomic. Already, we deal with something like that, purely within what’s currently the term level: * The same name may be used in different modules (and then I qualify) * The same name may be bound in different scopes (and we resolve via with shadowing) * The same name may be a record accessor in different records (and we resolve that with… eh, well, I have seen proposals about that ;-) So maybe there is a path towards a world where there is a single namespace, but we can deal with the same name referring to different things, where the resolution mechanism is ergonomic to use, and (unlike “type” and “term” sigils) does not keep the distinction between terms and types longer than necessary. If such a path exists I would be more confident that we can steer Haskell into that direction, given the plethora of punning libraries out there that should ideally continue to work ergonomically. Not sure how different “single namespace, but working with punning is ergonomic” is different from “two namespaces”. Maybe only in terms of framing and conceptualization. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/