[ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

[Vladislav Zavialov (int-index)]

> On 1 Jun 2021, at 15:12, Simon Marlow <marlowsd at gmail.com> wrote:
> 
> I'm hoping that what I'm suggesting could be done while still doing renaming strictly before typechecking. It's a kind of lazy name resolution - a name can resolve to a set of entities, and whether that is actually ambiguous or not is decided later during type checking, when we know whether we need to resolve the name in a value or a type context. Does that make sense?


Yes, I see how this can work, but if name resolution returns a set of possible entities rather than one, it means it hasn’t actually done name resolution completely. After all, not doing name resolution at all is also equivalent to having a set of names – if the user refers to a variable by its name “x”, then we already narrowed down the set of possible bindings from “all bindings” to “bindings of variables named ‘x’”. But name resolution is complete only when we find out which “x” exactly is referred to.

So this idea of lazy name resolution seems to amount to some name resolution prior to type checking, and then some more during type checking. It might be possible, but it does not strike me as "renaming strictly before typechecking”.

I worry that it might cause some trouble in other parts of the compiler. Dependency analysis of declarations comes to mind. Let’s say the user defines:

data A = B …
data B = A …

Currently we can process these declarations independently, there are no mutual dependencies. But if we postpone namespace selection, then this will become a strongly connected component, which will affect kind inference. I conjecture a more realistic example could be produced, but my goal is to simply state that weakening name resolution will have non-negligible impact on the implementation.

Implementation aside, the lexical scoping principle to which I referred is also about user expectations. When reading and writing code, I don’t want to inspect types just to figure out which name refers to what binding. It should be deducible from the lexical structure of the program.

So, while the idea sounds attractive, and it might be implementable, one would have to abandon the lexical scoping principle to pursue it.

> On 1 Jun 2021, at 15:12, Simon Marlow <marlowsd at gmail.com> wrote:
> 
> Not being able to use `[Int]` where a type is expected would be a serious drawback in my opinion, and I don't like the other alternative either: use `List Int` everywhere (rewrite all the Haskell textbooks!).
> 
> Cheers
> Simon

I share your disappointment, but it’s not as bad as rewriting all Haskell books! We continue to support the old syntax in all the old places, so code examples from the books will continue to compile. At the same time, codebases that lean strongly towards intermixing terms and types might adopt a different convention and require writing `List Int` everywhere. It could be part of a project style guide, for example.

Also, it is interesting that you say ‘where a type is expected’, because I there are at least three ways to interpret this:

1. Syntactically, a type is what follows after `@`, `::`, etc.
2. Things of kind `… -> Type` are types, things of other kinds are data. So `Bool` is a type, while `True` is data.
3. Erased things are types, so forall-quantified variables stand for types, while lambda-bound variables stand for terms.

Interestingly, under the first interpretation, `[Int]` does stand for the type of lists under this proposal, so I imagine it’s not what you meant. The choice between 2 and 3, on the other hand (and if we did lazy name resolution as you suggested earlier), would determine the meaning of programs such as:

  import Type.Reflection

  data True

  kindOf :: forall a -> Typeable a => String
  kindOf a = show (typeRepKind (typeRep @a))

  main = print (kindOf True)

Should this program print “Bool” or “Type”? Under (2), it must print “Bool”, because “True” is first of all data. Under (3), it must print “Type”, because the input to ‘kindOf’ is forall-quantified and erased.

Even if we partially postpone name resolution until type checking, there’s a lot of design space to explore (and to explain in the User’s Guide! this is not straightforward).

Under (1) it prints “Bool”, and name resolution remains blissfully unaware of any types involved.

- Vlad