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

Wed Oct 27 09:05:49 UTC 2021

There are a lot of inconvenient side effects and corner cases

Arnaud, could you enumerate them?  Even if (as I strongly hope) we accept this proposal, it's good to have a concrete list of things to bear in mind.   I for one do not have such list in my head.

One principle that the proposal espouses (but perhaps does not call out explicitly) is that it should be possible to write an explicit binder for every in-scope variable.    So instead of
                data T (a :: k -> k) = ...
I want to write
                data T @k (a :: k -> k) = ...
with an explicit binder for k.

So I see the proposal as removing an ad-hoc wart in the language.   But I may be blind to the "inconvenient side effects and corner cases" and I'd welcome a list of such cases.

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point simonpj at microsoft.com<mailto:simonpj at microsoft.com> will cease to work.  Use simon.peytonjones at gmail.com<mailto:simon.peytonjones at gmail.com> instead.  (For now, it just forwards to simonpj at microsoft.com.)

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Spiwack, Arnaud
Sent: 27 October 2021 09:20
To: Richard Eisenberg <rae at richarde.dev>
Cc: ghc-steering-committee <ghc-steering-committee at haskell.org>
Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

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<mailto: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<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F281&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688770920%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9k5jhyoKPDXal1oQoahl7CDReJtVVK3yet1a82td1KQ%3D&reserved=0>
Proposal text: https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall%2Fproposals%2F0000-visible-forall.rst&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688780863%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=VBNE3eXKhJKDonDrfeuWoLTWaBsINs5TLPrghtYAdkc%3D&reserved=0>

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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst%23lexical-scoping-term-syntax-and-type-syntax-and-renaming&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688790833%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=GuMiExefsGrYT8qkQZe1rgmo42M%2By0TDOrEmyXUNcoQ%3D&reserved=0> 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fdependent-types%2Fproposals%2F0000-dependent-type-design.rst%23dependent-application-and-the-static-subset&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688790833%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=VN1vQ77CVUD1Fe9XNfHMzztv%2FD9Jxkt8CjgJtl%2F9w8Y%3D&reserved=0>. 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<mailto: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<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fpipermail%2Fghc-steering-committee%2F2021-May%2F002454.html&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688800785%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=EsMkJHvCNi30T%2FUneEyJ6mblBO9%2BXv1HUNJGJTSxOy4%3D&reserved=0>

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<mailto: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:<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0378-dependent-type-design.rst%3A&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688800785%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2HE8XEL%2FE4rNvMYcUgmPiNI4NmWX5kO%2B6LhQXi%2FxXmQ%3D&reserved=0>

> 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<mailto:ghc-steering-committee at haskell.org>
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688810744%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=Cl00sfjlpg3xh2jTlToWAsJgBTUfqQcNS1ZxNn6utiI%3D&reserved=0>

_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee at haskell.org<mailto:ghc-steering-committee at haskell.org>
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=04%7C01%7Csimonpj%40microsoft.com%7C3f47d750845a4cdd4c1608d99922b5f8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637709196688810744%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=Cl00sfjlpg3xh2jTlToWAsJgBTUfqQcNS1ZxNn6utiI%3D&reserved=0>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20211027/55d316d5/attachment-0001.html>