Linear types amendment: Linear lets #624
Conversation
aspiwack
force-pushed
the
linear-lets
branch
from
8c58091
to
a1e381a
Compare
|
@aspiwack Maybe you forget to add Rendered link to your first comment |
I didn't: there isn't a rendered link because it's an amendment. Instead, go to File changed and choose to display the rich diff. I'm afraid there isn't a better way. PS: I had inadvertently included another proposal in this PR, I've fixed it as soon as it was pointed out to me. |
|
Except… the rich diff isn't working for me at the moment. Is it just me? Is it just my document? |
Doesn't work for me either at the moment |
|
Can you have multiple bindings in one let? As in let %1 x = u
%Many y = v
in … |
I don't see any reason not to. What makes you doubt it, so that I clarify in the proposal? |
Only the lack of such an example in the proposal |
|
I don't know what in my PR breaks the rich diff view, but I'm convinced at this point that it isn't transient. I've added link, in the PR description, to the various sections that I've added, hopefully I didn't forget any. |
|
The conversation died out. @nomeata I'd like to submit this proposal amendment to the committee. |
nomeata
added
the
Pending shepherd recommendation
proposals/0111-linear-types.rst
Outdated
|
|
||
| Non-variable linear patterns can't be lazy (see `Lazy patterns`_). As | ||
| a consequence, non-variable let-bound patterns must be annotated with | ||
| a ``!`` (because let-bound patterns are lazy by default, as opposed to |
There was a problem hiding this comment.
What happens if -XStrict is in effect?
There was a problem hiding this comment.
We still require a !. (we could do better, but it's unclear that it's worth it, especially since -XStrict is so rarely used)
There was a problem hiding this comment.
I've made a number of comments throughout. Many are simple typos or small corrections. Regardless, I'm in support of this -- especially because we are having debates about stability elsewhere, and thus seem to be carving out a space for more experimentation here. That is, maybe the interaction between generalization and the desire to infer linear bindings is a bit wrong in this proposal, something that will be hard to know until it's implemented. But that's fine: users of -XLinearTypes know that it's subject to change.
Small open question: how many users of -XLinearTypes do we have? If it's "lots", then this might want a new -XLinearLets extension that's less stable. But if it's "not that many, and we're friends with most of them", let's just keep it simple in one extension.
| -- Doesn't work | ||
| let %p f x y = rhs in body | ||
|
|
||
| instead write |
There was a problem hiding this comment.
What's the reason for this restriction? It seems surprising.
There was a problem hiding this comment.
Honestly, I haven't really given it any deep thought. let x :: sig is a PatBind in the implementation, I made let %p x a PatBind too. It's a more minimal change in the code base. Like previous comments: this choice is conservative and doesn't prevent from extending the syntax when we have more experience about it.
| But this means pattern-matching on a lambda abstraction (albeit a lambda over | ||
| type variables), which is not something that Core understands. Also, ``f`` and ``g`` | ||
| should be polymorphic, despite the fact that both fields of ``p`` are | ||
| monomorphic. It's not clear that this makes sense. Even assuming that it makes |
There was a problem hiding this comment.
This bit is true regardless of linear lets and such. The fields of p are monomorphic, but the type they work on is a variable, bound in an outer big lambda. This point is not important for the proposal, though.
There was a problem hiding this comment.
Right. The point was that the way we work around it for unrestricted bindings doesn't work for linear types. And that the way we compile linear pattern bindings doesn't apply to this situation.
| prevents the type-checker from generating ``AbsBinds``, and, as such, | ||
| makes more inferred lets linear, which is almost certainly the right default | ||
| (at least it's the least surprising: a binding doesn't change from | ||
| linear to unrestricted because a small change makes it generalisable). |
There was a problem hiding this comment.
I fear there is trouble here, because MonoLocalBinds is not as powerful as you think.
This also clarifies that annotated variables (which do not get the AbsBinds treatment) and polymorphic field projections are just fine. That's good. But I do think that there will remain a tension between inferring a linear binding and generalization.
There was a problem hiding this comment.
I can't deny that there is this nagging part of my brain that suspects that maybe something is still amiss. But I haven't been able to find an issue yet.
proposals/0111-linear-types.rst
Outdated
| patterns are monomorphic`_) that | ||
|
|
||
| 1. ``-XLinearTypes`` implies ``-XMonoLocalBinds``. | ||
| 2. Polymorphic non-multiplicity-annotated let-bound non-variable patterns are inferred to be unrestricted |
There was a problem hiding this comment.
I think this isn't quite what you mean. I think you just want to say that generalized bindings are unrestricted. If a binding binds a polymorphic variable without generalization, then it's fine.
There was a problem hiding this comment.
I changed “Polymorphic” to “Generalised” hopefully this is clear.
| are annotated with ``%Many``. But it invites a lot of complication | ||
| (what if it's a type synonym that is equivalent to ``Many``? What if | ||
| it's a type family?) that are hard to justify. In particular since we | ||
| take ``-XMonoLocalBinds`` for granted, where generalisation doesn't |
There was a problem hiding this comment.
Again, this last point isn't accurate, but it doesn't matter. I'm fine with let %Many disabling generalization. If you want it, just use a type signature!
Co-authored-by: Richard Eisenberg <rae@richarde.dev>
|
@goldfirere in addition to the threads above, the part about generalisation vs linearity was born of the implementation. I hadn't realised the tension prior to implementing all this. |
nomeata
added
Pending committee review
|
OK. I declare this accepted. |
adamgundry
added
Accepted
Would be best consumed using the rich diff view, except it doesn't appear to work. Fortunately, this is almost entirely added section, so I can point to them individually.
LinearTypesis proposed to implyMonoLocalBindsThis is a rather straightforward amendment which specifies multiplicity-annotated let bindings which, for reasons unknown to me, were only implied before. Pretty much all the choices are forced, the design space is really tiny. In consequence I intend to leave this open for comments a few work days before I submit it to the committee.
@simonpj , you may want to take part of the pre-committee reviews.