Linear types #91
Linear types #91
Conversation
With great inputs from @facundominguez, @mboes, and @jyp
A few nits found while reading the proposal. I fixed a few things that didn't render correctly on github, maybe it's just their rst renderer being nazi, in which case I can remove them from the pr.
Fix typos and syntax errors
Does discouraged syntax mean the syntax without the tick? (i.e. |
|
@phadej yes, that's what I meant. |
|
typo: levitiy |
|
I'd like to see a comparison to GHC's previous attempt at linear types, the Linear Implict Parameters extension, which was available in GHC versions 5.04 to 6.4. Since LIP was eventually removed from GHC, it would be useful to know what the problems were and how this new proposal fixes them. |
|
I voiced my complaints on Reddit, but in the name of meritous discussion I'm posting a copy here, too. I hope they don't come off as harsh, but as a serious evaluation of the potential of this proposal. This change is extremely big and will have (I am certain, from experience) unforseen consequences and interactions down the line, and due to the fact it can change so much of the surface language, I think careful examination is important. That doesn't mean it shouldn't happen, but the bar is damn high. (And I know that I'm an old fart who isn't really involved as much anymore, so I have little weight, but I still think this is an important point to answer.) (And if I missed something obvious that is either addressed here or in the recent papers, I'd appreciate a pointer and I'll shut up.)
|
|
How much is there for commenting on this before any decisions are made? I am very interested in engaging in the discussion, but do not have time immediately. |
|
Overall, I'm +1 on this. It has motivating use-cases and has been thought out well. Here are several unrelated thoughts as I read through the proposal: First thought: I like that Next thought: The array functions have the following type signatures: Why is the result wrapped in
So as a function argument, Do they or do they not? If they do, Next thought: I like that there are no proposed changes to Next thought: I like the syntax for specifying multiplicities. It's ugly, but it's less ugly than anything else I can imagine. I'm glad that the "unification of multiplicities will be performed up to the semiring laws". Next thought: I'm not convinced that 0-multiplicity arrows carry their weight. According to the proposal:
Later in the proposal, a complication is noted:
That's pretty strange. I would expect something polymorphic in That's all. Great paper and great proposal. I look forward to whatever form this eventually takes when it makes it into GHC. |
Plenty of time. Many of the GHC proposals are about very specific things with purely local effects. This one would be a big and fairly experimental change, and needs careful discussion. So you have time! Meanwhile, I urge everyone on this thread to read the paper; it's linked from the proposal. Without the paper I doubt that you'll be able to make much sense of the proposal; it's pretty much essential to an informed disucssion. (Of course it doubtless has shortcomings too, but that's partly why Anaud has turned it into a proposal.) |
|
I remember that there were several versions of “the paper”. Where can I find the final version, which I guess is the one I am supposed to read? |
|
You can find a link in the proposal (second para). DO NOT read our ICFP submission. The POPL version (at the above link) is a total rewrite. Simon |
|
typo: s/scrutiny/scrutinee/
The idea looks terrific. Because the impact is big, does implementing it mean freezing all other type-related development while type inference is lying on the operating table having open heart surgery? I'm thinking particularly about the interaction with Type-in-type, Type-level type application, visible dependent quantification. |
|
I have a number of concerns with this proposal as written
1) linear types are unsafe/unsound in the presence of (pure or even
impure!) exceptions, especially for the sorts of resources of interest
here! This proposal emphasizes examples like sockets, but doesn't address
that issue! This also creates a channel for space leaks of linear values if
there was a linear heap!
I guess this ties into why Rust does abort only / unrecoverable exceptions!
whats our story here? currently its a total gap in the paper and the
proposal!
2) i notice that the treatment of irrelevant/linear/intuitioninistic
terms/types (ie 0,1,Omega), aka "multiplicities", use the arithmetic style
from the work of conor mcbride and bob atkey! I agree that its very nice
stuff, but theres some substantial issues with going from that model of
multiplicities to the usual one we expect (the subtyping relation there
only works cleanly when omega means >1 usage, afaik! theres ways around
that, but they create a LOT of complexity that i'm not sure is actually
necessary). I've explored some of the alternative lattice choices that you
can do, but they all kinda force your to drop the +/* arithmetic approahc.
(also i couldn't find which page in the popl draft on arxiv talks about
your particular choice of multiplicities).
Roughly: every location that expects something at multipliciy 0 as an
argument should/must be able to accept a type compatible value of
multiplicity 1 or Omega, but as written i'm not sure if your fomulation
permits that. (this is an issue for the mcbride and atkey systems in my
mind). Addressing this changes the lattice structure, which impacts how
you might do type inference or multiplicity generics!
3) what linearity optimizations are safe in the presence of catchable
exceptions? what type safety properties related to linearity still hold in
the presence of (catchable) exceptions?
4) I have some concerns about tuples: why can't i have a mixed multiplicity
tuple? (a simple issue seems to lurk in your data type model, but i'm still
digesting that)
5) how will multiplicities interact with unboxed tuples? What would be the
type of an IO monad with a linear state token?
6) AS written, a function type has only one multiplicity parameter, f : a
-p-> b . This is misleading notationally!
6a) in f : a -p-> b, p only refers to the multiplicity of the function
argument of type a, and perhaps the result of type b! the multiplicity of f
is in the parent scope!
6b) you actually want to write something more like f:_p1 a_p2 -> b_p3, or
something to that effect! this especially matters when you start dealing
with questions about functions that take and return unboxed tuples, or how
this all interacts with core such.
7) how does the semantics for linearity as intended here relate or not to
the approximate usage analysis annotations in ghc core?
8) I actually find that theres a pretty natural way to add Par and External
Choice linear logic operators to a concurrent functional type system, do
folks at tweag have any plans in that direction? (some parts of semantics
and types get much cleaner and easier to extend with this setup i've found)
these are just some off the cuff questions, :)
…-Carter
On Thu, Nov 9, 2017 at 6:04 PM, AntC ***@***.***> wrote:
typo: s/scrutiny/scrutinee/
@simonpj <https://github.com/simonpj>
This one would be a big and fairly experimental change ...
The idea looks terrific. Because the impact is big, does implementing it
mean freezing all other type-related development while type inference is
lying on the operating table having open heart surgery?
I'm thinking particularly about the interaction with Type-in-type,
Type-level type application, visible dependent quantification.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#91 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAAQwki_Cgbla6zmpSaO2PLvVWFO8fpYks5s04URgaJpZM4QYEht>
.
|
|
Re: In the case of the array, it enforces well-scoping of the linear arguments: the linear arguments are not accessible passed the scope because they can't be returned as part of the |
No. Like any other feature, work on prototyping linearity will have to go in parallel with everything else. |
|
@thoughtpolice if you're going to bring the reddit thread in, then let me paste a link to your original comment thread: https://www.reddit.com/r/haskell/comments/7bulxb/linear_types_ghc_proposal/dpl6r2n/. It already includes answers to many of your points. |
|
Addressing your points (sorry about the weird formatting):
6a) Only to the argument.
|
|
Copying over the answers to @thoughtpolice from the reddit thread for posterity: @jyp wrote:
@mboes wrote:
|
|
@gbaz I’ve read the article Affine Sessions which you cited above. I don’t think this paper supports your case: failures are explicit, and have an operational behaviour. In other words, these affine session types live in an ambient linearly typed world: it is not the case that you can silently drop a variable in this system. Really, it behaves more or less as a linearly typed language with exceptions (with some variations due to the specific domain under study), which is essentially what we are proposing for |
|
Here is the situation I’m was worried about: -- Let’s assume a function `fill` which sets all the cells of a mutable arrays
fill :: MArray Int ->. MArray Int
-- `uarr` is unrestricted because its definition does not have any free variable
let uarr = newMArray (\arr -> freeze $ fill arr)
in
forkIO $ return $ case uarr of { Unrestricted a -> a }
case uarr of { Unrestricted a -> a } -- I can force `uarr` twice in parallelMy worry was that if the At any rate, we are in a simpler case than |
|
@aspiwack Wait, are we going to have to use a different arrow for linear lambda? I feel like that should be option if the compiler can infer that the lambda has to be linear from the use site. |
Yes, that is right. We'll lose sharing, but it is a different story. |
|
There was another point made by @rleshchinskiy about linear types, apart from the typing of
It was noted already that getting the types right for primitives is a tricky business. But I want to point out that the same applies if we have affine types instead of linear types. If a primitive is not morally linear but is given a linear type, type preservation can be destroyed, as previously observed by @rleshchinskiy. If a primitive is not morally affine but is given an affine type, type preservation can likewise be destroyed. In fact this very point came up earlier in the discussion. In an earlier comment, @gelisam points out that the type for fill :: a ~>. D a ~>. ()But that's a mistake. This particular function should have signature fill :: a -> D a ~>. ()In fact, because with the wrong signature for dup :: a ~>. (a, a)
dup x = case ul with Unrestricted l -> (head l, head l)
where
ul = allocList (\dlist -> let !(da, dtail) = consD dlist in nilD dtail `lseq` fill x da)
lseq :: () ->. a ->. a
lseq () x = xthis mistake should have the consequence of breaking type preservation for affine types. Of course, direct-style affine typed functions offer fewer guarantees to their caller. So of course, it's harder to step into the danger zone where preservation is compromised. But that's just the same old story from PL theory: the stronger your types, the sooner you break preservation if you're not careful. |
|
@Sahgher no, sorry, that was a typo. I'm rather in favour of being able to declare linearity at the lambda site, but this would be a misleading syntax (as we still want |
|
@aspiwack First of all, I'd like to clarify that I really like the ideas put forth in the paper, it's great work. It's just seems to me that they work better with affine types than with linear ones. Secondly, we really need actual examples of interfaces we want to be able to provide at this point. I will try to address some of your points but I do feel that we're starting to go in circles and having some actual code as a basis for the discussion would help a lot.
I don't think anyone doubts that. However, they can also be implemented without linear types so the question really is what linear types buy us beyond what we have now. It seems that we get the strong guarantee that we don't use resources after they've been freed. This is very useful but it is an affine guarantee, not a linear one. What other guarantees do we get?
So far, we've had one example which essentially relies on relevance: 3D models. We need Haskell code for this one and we need more use cases to see what situations relevance matters in. Things are made more complicated by the fact that we aren't getting true relevance (because of exceptions) so just taking standard examples from the literature doesn't necessarily work (as we've seen in the case of resource safety).
As far as I'm concerned, not having a
I really don't propose to abandon anything, I'm not sure why you got that impression. I very explicitly said that in my view, having As to how natural expressing linearity is, I don't think that argument can be made without working through a few complete examples. However, I'd like to make two observations here. Firstly, I used Secondly, it is well established (starting with Wadler's paper) that the So again, this discussion needs real, fleshed out examples. I can't really address any of your points without those.
Because I think that with the approach you propose, an affine And with my Steering Committee member's hat on, of the 3 examples given in the Motivation section, the |
Okay, I'll download tweag's docker image, write a concrete implementation, and post it here when I'm done. Also I have a few other substructural examples in the readme of my category-syntax repository; since you're looking for more example, would it be worthwhile for me to attempt to implement those as well, or would it be better if the examples don't all come from the same person? |
|
@rleshchinskiy thank you for your continued input. @jyp announced here that the proposal authors are revising the proposal with extra content based on the feedback so far. Seeing as this latest round of discussion doesn't seem to have made any tangible progress as you yourself point out (in particular the discussion about Meanwhile,
@aspiwack and I already invited you to collaborate on some code samples, after you said
@aspiwack has since created the linear-base repo. I'd invite you to work with him there, specifically on a basic implementation of @aspiwack will close this PR in the meantime and resubmit with an updated proposal, in an effort to make it easier for others to join this discussion as well. Finally, I do have a request for clarification for the Committee. @nomeata, might you be able to bring this up with them?
|
Here's my view FWIW.
The proposals process does yet not give Core a special role in this way; but I'd argue that it should. |
|
I have finished my implementation of watertight 3D models. Having now used linear types in anger, I have quite a few pieces of feedback I would like to share.
Does that mean I should post the aforementioned feedback on the new proposal once it is posted, or should I post in now so it can inform the new proposal? My feedback has nothing to do with exceptions nor affine types.
I wasn't aware of that effort, so I wrote my own linear version of many standard things. I'll contribute my definitions there if they aren't implemented already. |
|
@gelisam Please share your feedback, it would be a shame to hold it for a while. We can copy or reference it in the new thread later.
Thanks |
Indeed, this is what the paper does. So what should the proposal do? Simply point to the paper's formal account? Name which extra fields with what type are added to which Core constructor? That is, from the moment that we have a paper formalization, be it a simplified Core (that ignores orthogonal features like coercions and polymorphism), is that all that is needed, or should we be discussing implementation details related to Core? If say optimizations are affected, should we be listing those too, even if this is the kind of thing that only gets discovered with an upfront implementation of the feature? Feedback much appreciated. But I suggest pushing any answers to the above question a PR with a diff to the ghc-proposals README. Best to have this meta-discussion elsewhere than in this (now closed!) ticket. |
|
All right, so here is my feedback. First of all, I like Second, a relief: given the definition of linearity in terms of evaluating terms to head normal form and such, I expected I would have to worry about strictness a lot, but I didn't end up having to use Third, a concern. I found it quite difficult to get linear type signatures right, and I wonder if it's simply because I am new to them or if there is a more fundamental problem. The reason I think it might be the latter is that when I got the type signature wrong, I didn't simply get a type error and had to try again, instead I managed to get quite a lot of code past the linearity checker before ending up in a dead end and having to try again with a different type signature. The specific case I am thinking of is my StateL implementation. To demonstrate how non-obvious this is, here is an exercise: think of a version of the State monad in which variables bound by My first attempt was So I switched to the other possibility, It turns out that Finally, I noticed that what I want from linear types in a library like this one is to force the users of my library to use my API linearly. Inside my library's implementation, I have a specific meaning of "to consume" in mind which has nothing to do with forcing values to normal form. As a result, I expect this pattern of hiding an Unrestricted value behind an unexported constructor to be quite common. It's an annoying representation because I can't use some typeclasses within my library implementation for fear of exposing them to my users. Maybe I could use the ST trick, asking my users to write code which works for any type I have a few more usability comments, but since they are related to the state of the linear types implementation and not the proposal, I'll find another place to post them. |
|
Third, a concern. I found it quite difficult to get linear type signatures
right, and I wonder if it's simply because I am new to them or if there is
a more fundamental problem.
To me it means that linear types are really useful: they help checking
non-obvious, non-local properties :)
My first attempt was s ->. (s, a), and using this representation, I
managed to implement instances for FunctorL
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/PreludeL.hs#L74>,
ApplicativeL
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/PreludeL.hs#L100>,
and MonadL
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/PreludeL.hs#L133>,
and also implementations for execStateL and modifyL. But then I tried to
implement getL, and I hit a dead end because getL :: StateL s s requires
a dup :: s ->. (s, s) under the hood.
IMO this shows that getL is not the right combinator. Normally, you want a
single piece of state threaded around, and you want to 'get' only the parts
of the state which are in fact duplicable. The rest of the time you'll be
using a linear 'modify'.
Finally, I noticed that what I want from linear types in a library like
this one is to force the *users* of my library to use my API linearly.
Not sure if I understand you fully, but one possible way out is to take a
unique linear context (which you can create using the CPS trick). Then you
make the entry points of your api take this linear context and output it
back.
Thanks a lot for your report!
|
|
Gelisam:
These are some great notes. I agree with the api design point you make.
I’d even go so far as to say that the tuple style encoding for mixing
multiplicies in your input and outputs is actually a very very important
technique for designs in this space. It also allows us to separately think
about the linearity of each curryable function application vs the
linearity if the arguments and results of each function!
…On Wed, Nov 29, 2017 at 10:35 AM Samuel Gélineau ***@***.***> wrote:
All right, so here is my feedback.
First of all, I like (->.) better than -o now. I implemented linear
versions of many existing concepts, and thanks to (->.) paving the way,
naming them was easy: prefix names get an L suffix, infix names a .. For
example, when I needed a linear version of Applicative, I named it
ApplicativeL and I named its methods pureL and (<*>.).
Second, a relief: given the definition of linearity in terms of evaluating
terms to head normal form and such, I expected I would have to worry about
strictness a lot, but I didn't end up having to use seq nor ! at all. I
now realize that due to the way in which linearity is defined, such
annotations should never be required. After all, a strictness annotation
could make it so that forcing a small part of the output forces a larger
part of the input than strictly necessary, but if all the parts of the
input are used somewhere in the output (which they must be if the input is
linear), then forcing the *entire* output to normal form (not just hwnf)
will of course force the entire input.
Third, a concern. I found it quite difficult to get linear type signatures
right, and I wonder if it's simply because I am new to them or if there is
a more fundamental problem. The reason I think it might be the latter is
that when I got the type signature wrong, I didn't simply get a type error
and had to try again, instead I managed to get quite a lot of code past the
linearity checker before ending up in a dead end and having to try again
with a different type signature.
The specific case I am thinking of is my StateL implementation. To
demonstrate how non-obvious this is, here is an exercise: think of a
version of the State monad in which variables bound by x <- ... with do
notation must be used linearly. For the regular State monad, the underlying
representation is s -> (s, a). Write down your best guess for the
underlying representation of this StateL monad. Got it? Okay, let's compare
with my implementation now.
My first attempt was s ->. (s, a), and using this representation, I
managed to implement instances for FunctorL
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/PreludeL.hs#L74>,
ApplicativeL
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/PreludeL.hs#L100>,
and MonadL
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/PreludeL.hs#L133>,
and also implementations for execStateL and modifyL. But then I tried to
implement getL, and I hit a dead end because getL :: StateL s s requires
a dup :: s ->. (s, s) under the hood.
So I switched to the other possibility, s -> (s, a). This time I was able
to implement FunctorL, execStateL, modifyL, and getL, but not ApplicativeL
nor MonadL. The reason is a bit complicated. Let's try to implement a
simpler function, pairL :: State s a ->. State s b ->. State s (a, b).
Even though the underlying f :: s -> (s, a) and g :: s -> (s, b)
functions are non-linear, we can only call each of those functions once. So
we call f s once, and we get back an (s, a) with multiplicity one. Which
is a problem, because we now need to call g on that s, but g wants to use
s with multiplicity ω. Another dead end!
It turns out that (->) and (->.) are *not* the only two possibilities
which need to be considered. The representation
<https://github.com/gelisam/linear-examples/blob/master/linear-common/src/StateL.hs>
which did work was Unrestricted s ->. (Unrestricted s, a), or
equivalently, s -> (Unrestricted s, a). This works because I can use s
non-linearly even when (Unrestricted s, a) has multiplicity 1. Is that
the underlying representation you wrote down? I'd be especially curious to
hear if those who are already familiar with linear types managed to get
that right.
Finally, I noticed that what I want from linear types in a library like
this one is to force the *users* of my library to use my API linearly.
Inside my library's implementation, I have a specific meaning of "to
consume" in mind which has nothing to do with forcing values to normal
form. As a result, I expect this pattern
<https://github.com/gelisam/linear-examples/blob/master/linear-watertight/src/WatertightL.hs#L73>
of hiding an Unrestricted value behind an unexported constructor to be
quite common. It's an annoying representation because I can't use some
typeclasses
<https://github.com/gelisam/linear-examples/blob/master/linear-watertight/src/WatertightL.hs#L98>
within my library implementation for fear of exposing them to my users.
Maybe I could use the ST trick, asking my users to write code which works
for any type u, and then within my implementation I instantiate u to
Unrestricted?
I have a few more usability comments, but since they are related to the
state of the linear types implementation and not the proposal, I'll find
another place to post them.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#91 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAAQwtZoEyqUT05qwrD6bZaWl3KTkIhxks5s7XnKgaJpZM4QYEht>
.
|
I am also much in favor of |
|
It seems really odd that type variables never stand for zero multiplicity as for every other type type variables of that type can contain any value of that type. Breaking this consistency doesn't seem like a good choice. |
|
If you followed this thread. You will probably be interested by #111 where the discussion continues with a revised version of the proposal. |
bravit
added
the
Non-proposal
This thread has been closed, however, a new thread discusses a revised version of the proposal at #111
This proposal introduces a notion of linear function to GHC. Linear functions are regular functions that guarantee that they will use their argument exactly once. Whether a function
fis linear or notis called the multiplicity of
f. We propose a new language extension,-XLinearTypes. When turned on, the user can enforce a given multiplicity forfusing a type annotation.rendered
By @aspiwack, @facundominguez, @mboes, and @jyp