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

[Spiwack, Arnaud]

I've been struggling to have an opinion on this PR. I'm very sympathetic to
the goal of the proposal (and this latest rendition of the proposal is a
really good document). There are a lot of inconvenient side effects and
corner cases (but, to be fair, these are not special to this proposal: they
are inherent to the dependent types plan). But I'm fairly convinced that
this is the best possible approach, or close enough.

So yes, I don't really feel strongly about it. But on balance, I think that
I'm in favour.

On Tue, Oct 12, 2021 at 9:05 PM Richard Eisenberg <rae at richarde.dev> wrote:

> This proposal has been revised for clarity, yet much of the payload is the
> same. I've just made a few small suggestions, but I believe we can
> deliberate here in parallel.
>
> To recap:
>
> Proposal PR: https://github.com/ghc-proposals/ghc-proposals/pull/281
> Proposal text:
> https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst
>
> The text of the proposal is long and detailed, but do not be daunted: it
> is simpler in practice than it appears.
>
> The main payload of the proposal is: Introduce a new extension
> -XRequiredTypeArguments. With this extension enabled, the `forall ... ->`
> syntax, currently in existence in kinds, is now available in types (of
> ordinary functions). This means that function definitions and call sites
> are sometimes required to write a type argument. The type argument is *not*
> preceded by @ or any other syntactic marker.
>
> This is useful for defining what would otherwise be ambiguous types.
> Example:
>
> sizeof :: forall a -> Sizeable a => Int
> sizeof = ...
>
> intWidth = sizeof Int
>
>
> There are further examples and motivation in the proposal.
>
> The rest of the proposal is simply about dealing with odd corner cases
> that come up with the main payload. In particular, mixing types in with
> terms with no syntactic signifier means that we must be careful about
> parsing and namespaces. If a type argument is written in the syntax that is
> shared between types and terms (including function application!) and uses
> identifiers in scope in only one of the two namespaces, nothing unusual can
> be observed. But, of course, there are corner cases. Here are some of the
> salient details:
> - Define type-syntax and term-syntax, where the choice of syntax is always
> driven by syntactic markers, such as :: or @. See the dependent types
> proposal
> <https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#lexical-scoping-term-syntax-and-type-syntax-and-renaming> for
> more details. Parsing and name-resolution are controlled by whether a
> phrase is in type-syntax or term-syntax. For name resolution, if a lookup
> fails in the first namespace (the term-level namespace in term-syntax or
> the type-level namespace in type-syntax), we try the other namespace before
> failing.
> - One unfortunate consequence of this extra namespace looking is around
> implicit quantification. If we have `a = 42` in scope and write `f :: a ->
> a`, that `a` will *not* be implicitly quantified. Instead, the user will
> get an error about the appearance of a term in a type -- but only if
> -XRequiredTypeArguments is on. This change affects no current code, but it
> does make the extension fork-like, in that enabling the new extension is
> not conservative.
> - Because term- vs type-syntax is controlled by syntax, a required type
> argument is in *term*-syntax and gets name-resolved *as a term*. In the
> absence of punning, this works out fine, but it is possible that a punned
> identifier will cause confusion. The proposal allows users to write `type`
> to signify a switch to type-syntax.
> - The proposal also includes a way to avoid punning for the built-in types
> with privileged syntax: lists and tuples. This method allows users to
> specify -XNoListTupleTypeSyntax to disable the list and tuple syntax in
> types (but still allows it for terms). The proposal also suggests exporting
> type List = [] from Data.List and other synonyms for tuples from Data.Tuple.
>
> ---------------
>
> I recommend acceptance. When doing type-level programming, the lack of
> this feature is strange, leading to ambiguous types and easy-to-forget
> arguments and easy-to-make type errors. The design space here is difficult,
> but this proposal is very much in keeping with the design sketch of our
> recently-accepted #378, in particular its section on this point
> <https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#dependent-application-and-the-static-subset>.
> I believe the design described here is both backward compatible with what
> we have today (users who do not use this feature will not notice a
> difference) and forward compatible with a cohesive design for dependent
> types.
>
> The "unfortunate consequence" above is, well, unfortunate, but I think it
> is unavoidable in the context of #378 -- and it will not bite if the user
> avoids puns.
>
> It would be great to bring this long-running proposal to a conclusion, so
> I'd love to hear your opinions in the next two weeks.
>
> Thanks!
> Richard
>
>
> On Jul 19, 2021, at 3:22 PM, Richard Eisenberg <rae at richarde.dev> wrote:
>
> This thread has trailed off, having escaped the pen while the shepherd
> (me) was distracted (first by travel, then by POPL). I'd like to resume it.
>
> You may wish to refresh yourself on the content of the proposal, which I
> summarize in
> https://mail.haskell.org/pipermail/ghc-steering-committee/2021-May/002454.html
>
> My recommendation remains to accept, for the same reasons it was
> originally.
>
> This proposal is somewhat controversial (it has garnered 278 comments!),
> and so it would be ideal to hear opinions from as many of you as possible,
> even if the opinion is just to accept the recommendation.
>
> Simon M wrote the last email in the thread before the hiatus, with a few
> questions. I'll attempt these now:
>
> On Jun 7, 2021, at 4:19 AM, Simon Marlow <marlowsd at gmail.com> wrote:
>
> As a user I usually need to know whether I'm looking at a type or a term
> in the code. For doing renaming in your head, it makes a difference whether
> you're looking at a type or a term: the namespaces are different.
>
> Is it reasonable for that to apply to visible type application too? That
> is, are we assuming that the user knows they're looking at a type, or are
> we assuming that the user "shouldn't need to care", or something else?
>
>
> My answer: "shouldn't need to care". This is enshrined in the Syntactic
> Unification Principle (SUP) in
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0378-dependent-type-design.rst:
>
> > *Syntactic Unification Principle (SUP).* In the absence of punning,
> there is no difference between type-syntax and term-syntax.
>
> Here, "punning" means having the same identifier in scope in both terms
> and types. Forgetting about the possibility of punning, users shouldn't
> care about whether they're writing a term or a type. All syntax will have
> equivalent meanings in the two environments. The *only* challenge is around
> namespacing -- and the LSP says that, in a term, names should correspond to
> term-level entities.
>
>
> What could we do if we were allowed to treat types differently? Well, we
> already do various bits of magic in T2T. But we could also use different
> name resolution rules. That doesn't necessarily mean we have to defer
> renaming until during type checking: we could resolve each name twice, once
> for the term context and once for the type context, and then pick one of
> these later when we apply the T2T mapping.  (earlier Vlad objected to this
> idea on the grounds that it might introduce spurious recursive
> dependencies, though).
>
>
> We *could* do this, yes, but it's in violation of the LSP (and, perhaps,
> the SUP). Of course, we wrote the LSP and can choose to break it, but, like
> Simon PJ, I think the ability to resolve names in the absence of
> type-checking is very valuable to readers of code.
>
> --------------
>
> One development on the GitHub tracker that may be of interest:
>
> @AntC2 proposes a migration trick to allow functions to migrate from
> today's world to a world with this new feature. The key example is sizeOf.
> Today, we have
>
> > sizeOf :: Storable a => a -> Int
>
> where the argument to sizeOf is always unevaluated and ignored. The
> proposal under consideration would allow this to change to
>
> > sizeOf' :: forall a -> Storable a => Int
>
> (NB: do not get distracted by the movement of the constraint, which will
> be invisible at usage sites) The problem is that we would have to make
> sizeOf' a new function, likely exported from a new library, in order not to
> clash. This is annoying. So @AntC2 proposes (in my paraphrasing, which
> @AntC2 has agreed with):
>
> * With -XNoRequiredTypeArguments, if a function f takes a required type
> argument of kind Type, then instead you can pass an arbitrary expression.
> f is called with the type of that expression; the expression is never
> evaluated.
>
> This would allow, e.g. sizeOf True to work with both the old and the new
> types.
>
> I am against this little addition, because it's narrowly applicable and
> has negative educational consequences (that is, someone encountering the
> type written for sizeOf' but then seeing sizeOf' True work correctly will
> be quite befuddled and likely form a misunderstanding of how forall ->
> works). Yet I can see this idea's appeal, thus my mentioning it here.
>
> ------------------
>
> It would be great if I could hear from everyone on the committee in the
> next two weeks with their opinion about accepting this proposal.
>
> Thanks,
> Richard
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
>
> _______________________________________________
> 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/20211027/a5a54cee/attachment.html>