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

[Richard Eisenberg]

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