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

[Simon Marlow]

On Sat, 29 May 2021 at 14:19, Vladislav Zavialov (int-index) <
vlad.z.4096 at gmail.com> wrote:

> Both of your suggestions (regarding lists and regarding Proxy) seem to
> require type information in order to resolve the meaning of an expression.
> Given `f e`, I’m assuming you want to parse/rename ‘e’ as an expression if
> ‘f’ is an ordinary function, and as a type if `f :: forall a -> …`.
>
> However, that would violate the Lexical Scoping Principle described in
> section 4.3.1 of the "Design for Dependent Types” proposal (#378), which
> states: "For every occurrence of an identifier, it is possible to uniquely
> identify its binding site, without involving the type system.”
>
> This principle is useful both in the implementation (it enables a clear
> delineation between renaming/typechecking) and when reasoning about
> programs. While it’s possible to violate it, I believe that writing `f
> (List Int)` is the lesser evil. Also, I don’t think that you’d need to
> "write `List Int` when it's a visible type argument, but `[Int]` everywhere
> else”. If consistency is an explicit goal, one can write `List Int`
> everywhere.
>

Admittedly I might be unfamiliar with a lot of the finer details here (I
haven't been tracking the dependent types proposal closely), but 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?

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



>
> - Vlad
>
> > On 29 May 2021, at 14:15, Simon Marlow <marlowsd at gmail.com> wrote:
> >
> > I support the goal of this proposal; indeed I would immediately use it
> in several places that I can think of off the top of my head.
> >
> > But the name resolution aspects concern me. I forsee a lot of confusion
> if we can't write `[Int]` as a type argument with the usual meaning. The
> error message is likely to be super confusing if it has to talk about the
> difference between a promoted list type and the usual list type
> constructor, which have the same syntax. I'm not a fan of having to write
> `List Int` when it's a visible type argument, but `[Int]` everywhere else.
> >
> > Would it be possible to require the leading quote to get the promoted
> meaning, otherwise defaulting to the usual meaning of `[Int]`?
> >
> > Also could we defer name resolution until type checking for things like
> `Proxy`, so that the obvious thing doesn't require namespace gymnastics?
> >
> > Cheers
> > Simon
> >
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210601/a5c83e18/attachment.html>