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

[Iavor Diatchki]

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>
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>:
>
>>
>>
>> On Aug 28, 2018, at 9:32 PM, Vitaly Bragilevsky <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
> 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/a1d0e65f/attachment.html>