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

[Joachim Breitner]

Hi,

Am Montag, den 23.11.2020, 18:22 +0000 schrieb Richard Eisenberg:
> On Nov 23, 2020, at 3:10 AM, Joachim Breitner <mail at joachim-breitner.de> 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 at joachim-breitner.de
  http://www.joachim-breitner.de/