[ghc-steering-committee] Proposal #111: Linear Types

[Simon Peyton Jones]

I imagine the biggest trade off is that the current proposal allows for polymorphism in the multiplicity, while I was thinking maybe we could start without.
Yes, that’s a total killer.  Polymorphism is absolutely central to the design.  I don’t think the design would hold water at all with two distinct function arrows.

As I said before, though, perhaps we should not worry that much about the function space, and just go for it.
I support that (albeit of course I have an interest in this, as a co-author).

I’m imagining that, absent -XLinearTypes, we would suppress (a) linearity polymorphism (b) -o (printing it as -> instead.   Every program that is accepted today would still be accepted.    So the extra polymorphism in the function space would be invisible.

Where would you get a bump in that road?  Imagine you imported a function with type
              f :: (Int -o Int) -> Int
and applied it to a function that did not have linear type. Now, we MUST produce a type error: the imported function f may rely on the linearity of its argument.  But note that this could not happen without compiling f with -XLinearTypes.  So, if you don’t use -XLinearTypes, you won’t see any bumps.

Of course that’s an informal argument.  Let’s see.  But it convinces me enough to accept the proposal – subject (as Richard says, and true of any proposal) it later turns out to have unforeseen but unacceptable consequences.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Iavor Diatchki
Sent: 29 August 2018 07:51
To: Vitaly Bragilevsky <bravit111 at gmail.com>
Cc: ghc-steering-committee <ghc-steering-committee at haskell.org>
Subject: Re: [ghc-steering-committee] Proposal #111: Linear Types

I was thinking about a design where the linear arrow is a completely separate type than the normal function type.

 I think that a choice like that would probably require additional annotations on other declarations to indicate when the linear machinery would kick in.

For examplee, `data` declarations would need an extra tag to indicate that we should generate linear constructors, pattern matching, and single field selectors.

Similarly, to declare linear functions we would either require a type signature, or some sort of a tag on the lambda/function declaration to indicate that it is linear.

I haven't thought through all the details but this is what I was thinking about.

Essentially, the difference is that the current proposal keeps track of these tags automatically in the multiplicity of the function space and I was thinking of a design where these things are specified manually.

I imagine the biggest trade off is that the current proposal allows for polymorphism in the multiplicity, while I was thinking maybe we could start without.

I am not arguing for this alternative design as I haven't really thought through all the details.  I was just thinking of alternatives that leave the current function space alone.

As I said before, though, perhaps we should not worry that much about the function space, and just go for it.

I have some comments on the type functions for multiplicities, but I'll write them in the git hub.

Iavor




On Wed, Aug 29, 2018, 8:40 AM Vitaly Bragilevsky <bravit111 at gmail.com<mailto:bravit111 at gmail.com>> wrote:
Now I get it, thank you for clarification. I agree with your recommendation.

Vitaly
вт, 28 авг. 2018 г., 19:39 Richard Eisenberg <rae at cs.brynmawr.edu<mailto:rae at cs.brynmawr.edu>>:



On Aug 28, 2018, at 9:32 PM, Vitaly Bragilevsky <bravit111 at gmail.com<mailto:bravit111 at gmail.com>> wrote:

I don't understand the meaning of "the road towards acceptance". Doesn't it mean discussing the proposal forever? I think we should accept it instead as it is or at least set strict timeframe for the final decision.

This is a good point. The truth is that the committee has no experience dealing with a proposal of the size of this one. It's hard (for me) to accept this proposal as is, because it's not a full specification. The big missing piece is inference. We also don't have a solid description of how much complexity the implementation will have to adopt. Yet, it would be very unfortunate for the authors to put in a ton of time into writing a paper, a proposal, and a prototype implementation only to get turned down. So, my understanding is that I'm recommending something of a conditional acceptance: we say, as a committee, that we're pleased with the general direction of travel and to encourage the authors to keep working. This means that we expect to accept, barring something large and unforeseen. The difference between conditional acceptance and outright acceptance is that it gives the committee further opportunities to suggest amendments to the proposed change. (Even an accepted proposal can effectively get retroactively denied if, say, the implementation requires a 10% slowdown on all programs to support an esoteric feature.)

Does this help to clarify?

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