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

[Simon Marlow]

On Tue, 1 Jun 2021 at 15:32, Vladislav Zavialov (int-index) <
vlad.z.4096 at gmail.com> wrote:

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

Don't we already do this for DataKinds? The lexical scoping rule is
slightly cheating with respect to DataKinds because while we can resolve an
identifier to its binding site, the binding site in the case of a promoted
constructor is actually two binding sites :)


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

To clarify what I meant here - if we want consistency, where consistency
means referring to the type of lists of Int using the same syntax
everywhere, then this leads to List Int and having to rewrite the Haskell
textbooks. So all the options are bad: we either have two ways to write
list of Int (and in some places only one of them works), or we have
consistency but we're changing something fundamental (and to a worse
syntax). The third option, namely using the "type" prefix also doesn't seem
appealing, because I have to know when to use the "type" prefix. I could
use it all the time, but then that's not much better than the current
situation (@-prefix) and I also have to read code written by other people
who don't adopt this convention.

With regard to list syntax in particular, I guess I still don't understand
why we can't
* require a promoted list to be written '[Int]
* change the T2T mapping so that [Int] means "list of Int" rather than the
promoted interpretation

After all, DataKinds already recommends using the leading quote and not
relying on unquoted syntax.

or perhaps this is undesirable for some reason? Do you think the promoted
interpretation is more useful?

Cheers
Simon



> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210601/6ad75b12/attachment.html>