Linear types

[aspiwack]

The proposal has been accepted; the following discussion is mostly of historic interest.

---

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 f is linear or not is called the multiplicity of f. We propose a new language extension, -XLinearTypes. When turned on, the user can enforce a given multiplicity for f using a type annotation.

rendered

This proposal has already been through one round of review. If you are new to this, you don't need to read the conversation there: it has been integrated into this newer version of the proposal. For a full understanding of the proposal, reading the companion article is recommended. For a bird's eye view of the proposal, you can browse the wiki page.

If you already read the previous version of the proposal, here is a summary of the main changes:

• The main technical change is that we've removed the multiplicity 0 from the proposal: it adds quite a bit of complication, and was only useful in interaction with Dependent Haskell. Maybe. And it was too much complication for something which was only potentially useful. (0 is discussed in the alternatives, as help if it's ever needed)
• We added examples based on external contributions and on the linear-base library that we've been implementing to demonstrate the programming style that this proposal heralds.
• We discuss how (deep, multi) pattern-matching is type-checked.
• We added a discussion on linearity vs affinity.
• We expanded vastly the discussion on exceptions.
• We added a (beginning of a) discussion on the effect on Core-to-Core passes.
• We changed the policy regarding unrestricted newtype definitions and GADT syntax when the extension is turned off

By @aspiwack, @facundominguez, @mboes, @jyp and @simonpj

Ongoing discussion with the committee

• Defining consume exactly once: interaction with evaluation and primitive unboxed types
• Linear pattern synonyms
• Printing multiplicity
• Multiplicities in let bindings
• Case syntax
• Of the use of linear types and resources

[cocreature]

The rendered link should point to https://github.com/tweag/ghc-proposals/blob/linear-types2/proposals/0000-linear-types.rst. It currently points at the previous proposal.

[aspiwack]

@cocreature fixed. Thanks!

[Ericson2314]

This proposal points out the annoyance of CPS when arguing against affine types, but then forces CPS on us (as before) for many use-cases by not doing linear kinds.

[Saagar-A]

The removal of the zero multiplicity seems problematic because it basically forces the situation where type variables cannot stand for zeroes to preserve backward compatibility when a zero multiplicity gets added. I see this behavior as surprising and inconsistent with how type variables behave in general. Also, it prevents one from doing things one might expect to be able to do like composing functions with zero multiplicity. It seems better to me to take the extra complexity now for better future compatibility.

[cartazio]

i'm not sure how this revision actually resolves the concerns and issues raised in the previous discussion, especially if the only substantive technical change is the dropping of the zero multiplicity...

likewise, i see zero mention of how to handle possibly mixed multiplicity fields in data type definitions, which is lacking from the associated popl paper too :(

[gbaz]

On glance, I think it does resolve the issues I raised. It acknowledges the issues with exceptions, describes a semantics that is correct with regards to the proposed behavior (which the old one was not), and provides a discussion of the tradeoffs. So on a technical front I see it as an advance. People may disagree with the proposal for a variety of reasons, but it appears "correct" in the sense that it describes accurately a change, its semantics, and its consequences, so it is a much improved starting point for discussion.

[cartazio]

Some of the discussion around record types confuses me, because it seems to ONLY allow single field records as linear.

I actually have a large number of resource modeling examples where I want mixed multiplicity records.

In my own work, the way to reconcile the tension here is to have unboxed tuples be enriched with per position multiplicity

consider

data LinearFileHandle = LH {myHandle ::_1 C_Handle, filePath ::_omega String}

this describes a perfectly reasonable pattern where i want to be able to share the path info throughout a computation, but guarantee linearity (errrm, affinity in this proposal i suppose) for the underlying handle.

with unboxed tuples i can uniformly describe both the Direct style unpacking AND the cps eliminator

(i'll pretend for now that unboxed tuples are also telescopes so i can use type annotation notation to indicate multiplicities)

directUnpackHandle :: (#  _ ::_1 LinearFileHandle #) -> (# _ ::_1 C_Handle , ::_omega String #)


let  (# ch, filepathName #) = directUnpackHandle myLinearHandle 
   in 
  -- stuff using ch and file handle

the cps version is even simpler/worse :)

directUnpackHandle :: (#  _ ::_1 LinearFileHandle #) -> ((# _ ::_1 C_Handle , ::_omega String #) -> a )  ->  a 

you really really need unboxed tuples with varying multiplicities if you want to directly write these things instead of pushign them into case.

Likewise.... I dont see a clean treatment / clear exposition of how to define any nontrivial datatypes, even records or tuples, which have mixed multiplicities in this proposal... and I think those are very important for usability. Perhaps i'm overlooking something, but this does seem to be a serious gap :(

[cartazio]

an alternative (but I think ultimately more fragile / complicated approach) to mixed linearity records is whats done in the cogent language out of nicta/data61, where they keep track of the partial projected-ness of a linear record and its fields.

I also think this expressivness in datatypes is crucial for actually supporting meaningful direct / monadic style APIs

a good example of this {edit: this point of expressivness} from another source is the discussion in pages 8 and 9 of this paper https://people.mpi-sws.org/~dg/papers/aff-know.pdf by deepak garg which uses linear typed programs to describe authorization, and the underlying issue there is the lack of such "tuples", so they circumvent the issue by making the troubling operation a primitive in their logic/programming language.

[cartazio]

I would like to make sure that i can model something like that example from deepak garg in a linear logical haskell programming tool

[andrewthad]

Thanks for getting out a more comprehensive version of this proposal. I am glad to see the zero multiplicity gone.

I agree with the concerns @cartazio expressed about not being able to express tuples of mixed multiplicity. Changing unboxed tuples to somehow linearity-polymorphic would be a heavy-handed, breaking change since it would endow unboxed tuples with additional type arguments for multiplicities. I would like to suggest a simpler solution: adding an additional unary unboxed tuple whose data constructor is non-linear. This is a little hard to discuss because GHC currently doesn't have an exposed name for this data constructor, but it's internally called Unit#, so I going to go with that. What I am proposing is that we make the data constructor for Unit# linear, which is consistent with the proposals treatment of unboxed tuples, but that we add another unary unboxed tuple type named UnitOmega# whose data constructor is non-linear (note that Unit# and UnitOmega# are both the names of both a data constructor and of a type constructor):

>>> :k Unit#    -- the type constructor
r -> TYPE (TupleRep '[r])
>>> :t Unit#     -- the data constructor
a :-> Unit# a     -- linear
>>> :k UnitOmega#    -- the type constructor
r -> TYPE (TupleRep '[r])
>>> :t UnitOmega#     -- the data constructor
a -> UnitOmega# a     -- non-linear

Now, consider the example that @cartazio wrote with the fictitious multiplicity designations as:

directUnpackHandle :: (#  _ ::_1 LinearFileHandle #) -> (# _ ::_1 C_Handle , ::_omega String #)

If I understand the intent of this correction, I believe it could be expressed with UnitOmega# as:

directUnpackHandle :: LinearFileHandle :-> (# C_Handle, UnitOmega# String #)

Maybe UnitOmega could be best understood as an optimization for situations where the boxing introduced by Unrestricted is undesirable. It neatly sidesteps the problems that a non-linear identity newtype encounters because, unlike a newtype, it doesn't get turned into a cast in Core.

[AshleyYakeley]

repetition of "consumed exactly once"

[aspiwack]

Sorry. I must have missed something. But I don't see a repetition here.

[AshleyYakeley]

NM, I misread it.

[AshleyYakeley]

These rules imply x * y = y, surely this is wrong?

[aspiwack]

Right. The second one was supposed to be x*1=x (1 is neutral).

• Fix this.

[cartazio]

@andrewthad your proposed encoding would be at least spiritually, in that you're adding the linear logical exponential as UnitOmega#, a sort of special (levity polymorphic) no-op new type?

but this actually raises an important point: unboxed tuples do not exist after type erasure, and to quote the runtime rep data type thats now part of the kind system https://hackage.haskell.org/package/ghc-prim-0.5.1.1/docs/GHC-Types.html

TupleRep [RuntimeRep]  -- | An unboxed tuple of the given reps

we could easily enrich this to

TupleRep [(Usage,RuntimeRep)]  --  An unboxed tuple of the given reps and their Usage (linear/omega)

and have a typing rule that an unboxed tuple is a "linear" value wrt how you're allowed to eliminate it if it has any linear fields.

this would greatly improve the expressivity of the current proposal I think.

my point about erasure is perhaps a subtle one: unboxed tuples are exactly the calling convention / abi for haskell function calls and returns wrt register placement, they never exist on the heap!

(@andrewthad so i guess i'm ultimately disagreeing with you somewhat :) )

[Ericson2314]

@cartazio the "usage" thing looks good, but if we do that, lets just go full linear kinds (so that the type of the list elements once again matches the (uncurried) parameter type of TYPE). My CPS comment above was a bit cryptic, but basically I think to properly leverage linearity we want a full linear kind.

---

Contrary to the proposals and paper, Rust also has a linear (sub)kinds, and not uniqueness types. (It's immutable and mutable reference types exhibit a uniqueness-types-like subsumption relation, but this is a library/axiom phenomenon, not a fundamental property of the language itself.)

I'm very used to the full power of this in Rust, and it would be shame to have something inferior in Haskell. We can still perhaps do linear arrows as a sugar / convenience on top if we really want. I don't buy the integrating-with-existing-code argument. Many of use want to make unlifted/unboxed code more idiomatic and ergonomic, so we're already going to fight analogous battles related to other possible additional parameters of TYPE.

[andrewthad]

@cartazio What you describe is the more heavy-handed approach that I was wary of. I don't particularly like the idea of redefining TupleRep to talk about linearity, plus you need to invent new syntax to talk about unboxed tuples with non-linear arguments. Anyway, I wouldn't consider this a pressing issue since either of our solutions could be added later in a backwards-compatible way. In an ideal world, we would just have something like an UnliftedDataTypes extension that allowed us to define a mixed-linearity unboxed type as:

-- note: the Int consume linearly and the Word is not
data Foo :: TYPE (TupleRep '[IntRep, WordRep]) where
  Foo :: Int# :-> Word# -> Foo

Side note: my intent was that UnitOmega# be levity-monomorphic, not levity polymorphic. But I guess it may not actually matter.

[aspiwack]

Thanks for all your comments! Let me try to provide answers to every question.

@gbaz "correct" is good. But let's aim for "complete" as well. Don't hesitate to point out to what's missing or unclear. And if you have ideas to fill in the unresolved bits: please share!

@Saagar-A Dropping the 0 multiplicity was suggested by @andrewthad in #91 and after internal discussion, we dropped it from the proposal because it adds significant complexity, the "right way" to add to add the 0 multiplicity is still unclear, and we don't actually know for sure that we will need the 0.

So what happens if we add it now, in a clunky way, and discover later that it was never useful in the first place? I would be uncool. If we need to add the 0 multiplicity later, all the strategies which were proposed in #91 would still apply, maybe some of them would feel less palatable after the fact, but we would have concrete examples to work from!

@cartazio @andrewthad The proposal specifically adds data types with mixed-multiplicity constructor. Also the paper. There is no syntax for non-purely linear record constructors. But they are also discussed in the proposal. There is no technical difficulty, we simply don't have a syntax yet. (though thank you for bringing this up, I just realised that I didn't specify record patterns in the proposal)

I believe the the proposal also mentions mixed-multiplicity unboxed tuples: I believe them to be needed in the implementation (for the interested parties: I appear to need them to properly perform the worker/wrapper split for strict functions), but I don't have a syntax for them in the surface language. This could be solved elegantly by the UnliftedDataTypes proposal.

In the meantime, a single unlifted 1-uple of multiplicity ω (a consistent name for which would be Unrestricted#, though we may want to change the name Unrestricted to something shorter, as it comes up all the time) is not complete: we also need tuples with multiplicity a free variable. Though, I guess, a single Mult# :: a :p-> Mult# p a could do the trick.

• Specify record patterns in the proposal
• Add link to the UnliftedDataTypes page in the unboxed tuple discussion

[andrewthad]

@aspiwack Thanks for the response. I agree that the proposal is already clear on data types with mixed-multiplicity constructors. I had missed the discussion of mixed multiplicity unboxed tuples in the proposals in the proposal. For the interested parties, it reads:

It seems that, because of the worker/wrapper split in the strictness analysis, Core will need unboxed tuples with multiplicity-annotated fields. Even if there is no surface syntax for these in the proposal.

It would be helpful if this were reiterated in Section 1.2.8 Unboxed Data Types. Also, the UnliftedDataTypes proposal that you reference doesn't actually give us what we want here. It allows users to define more inhabitants of kind TYPE UnliftedRep, but we need to be able to create more inhabitants of kind TYPE (TupleRec xs). Otherwise, we'd still be paying the heap allocations that unlifted boxed types incur. I agree though that something similar to it would be the best way, in the long term, to offer some kind of surface syntax for mixed-multiplicity unboxed tuples. As a short-term easier-to-implement solution, I like your Mult# suggestion, which I believe would look like:

-- type constructor
Mult# :: forall (r :: RuntimeRep). Multiplicity -> (a :: TYPE r) -> TYPE (TupleRep '[r])
-- data constructor
Mult# :: forall (r :: RuntimeRep) (a :: TYPE r) (p :: Multiplicity). a :p-> Mult# p a

[cartazio]

the only two mentions i see are

a)

data Foo2 where
  Bar2 :: A ->. B -> C 

which i assume is a typo and should instead b e

data Foo2 where
  Bar2 :: A ->. B -> Foo2

b)

1.7.6   Binders with multiplicity
In the paper, we wrote λ x :₁ A. u for (unannotated) linear functions. We don't currently provide a corresponding syntax, for lack of good syntax.

If a syntax is provided, we could also use this syntax to have records with different multiplicities.

data R = R { unrestrictedField ::(Omega) A, linearField ::(One) B }

What is the semantics of the case (a) in the notation of case (b)

my expectation is that would be equivalent to something along the lines of (with currying removed to clarity)

data Foo3 where
  Bar3 :: ( One A , Omega B ) ->  Foo3)

phrased differently, for f :: ( a .-> b) has a different meaning in function land vs data type land, right?

f ::one (a .-> b) vs f ::omega (a .-> b)

I do think that putting the linearity info on the arrows of the data types instead of the fields of the datatype constructors does confuse reading them, since its how you construct the datatype determines its ultimate usage in the application, right?

i guess i'm just really really wanting user visible unboxed tuples with use annotations (which maintaining well typed worker wrapper will apparently need?) and a cleaner / more explicit notation for how to read mixed usage annotations per field in datatypes.

in purely linear / linear logical code, this doesn't matter, because linearity just composes everything! but our programming languages/reality live in world of both eternal mathematical truths and resources, and making sure talking about those cleanly is important for end users.

[cartazio]

for clarity i'm attaching the remarks from the depak garg paper that I think are relevant

and the full paper
A Linear Logic of Authorization and Knowledge⋆ Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning and Michael K. Reiter aff-know.pdf

[Ericson2314]

Also, the paper implies we'd need to use GADT syntax for virtually all data types to support the linear kind, but I don't see why we can't just infer it for non-GADT syntax (again as Rust does)

Code without -XLinearKinds would see any linear types, and would see all multiplicity-polymorphism specialized away (to Omega).

[cartazio]

.... you totally dont need GADT syntax, at least if you allow record field style annotations on the fields, as in their strawman syntax that they indicated isn't currently planned. (but is also a good example of not needing linear function spaces to define the types)

[cartazio]

@Ericson2314 i agree, gadt syntax shouldn't/needn't be required, it seems like a case of pushign the complexity into a small corner, which I think actually increases the complexity.

In my experiences, a curried linear function arrow is actually one of the most complex approaches you can do for linear logic.

in the following notation i use usageA/Bi to mean multiplicity, and Ai Bi are types sans usage
and usage0 is the binding multiplicity in context

f :: usage0 (#  :: usageA1 A1 , ...  :: usageAn An #) -> (# :: usageB1 B1  , ...  :: usageBm Bm #)

lets call this pattern of linear function LinearFunctionSpaceNotation (and assume Ai Bi can )

i can specialize this to LinearConstructorNotation (which kinda looks like a multi category?)

MkFooLooksSortaLikeAGadt :: usage0 (#  :: usageA1 A1 , ...  :: usageAn An #) -> (# :: usageB1 B1  #)

to exactly and CLEARLY describe the typing rules/type behavior of a single data constructor explicitly

and for a record or other constructor with multiple fields, i can do the opposite (lets call this LinearProjectionNotation)

projectBaz :: usage0 (#  :: usageA1  #) -> (# :: usageB1 B1  , ...  :: usageBm Bm #)

how do i write / encode these in the proposal today, or what syntax would be needed to be able to write general things of the pattern of LinearFunctionSpaceNotation . With that level of expressivity (ignoring the fact that this in its full generality requires some handling of type quantifiers/generics such as perhaps seen in the age old TypesAreCallingConventions paper https://www.microsoft.com/en-us/research/publication/types-are-calling-conventions/ https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/tacc-hs09.pdf), I can actually encode ALL the standard connectives of classical linear logic in a functional programming setting, and do some really cool modelling.

TL;DR with the current proposal,

how would i encode/emulate what i'm calling LinearFunctionSpaces? this has serious impacts on modeling expressivity

Is the datatype facility flexible enough to allow me to model Authorization data types with delegation?

This actually raises in turn an interesting/challenging question: can / should users be able to define sum type with arbitrarily varying usage choices per constructor that come up with describing interesting resources?

consider using linear logic to model some sort of enterprise / business authorization where you have "X is approved to do Y", "X can approve their choice of Z to do Y" and "X can delegate to new people Z (who may or may not be able to delegate futher) approving their choice of person A to do Y "

this is a pretty simple example of more complicated authorization systems that come up in practice, and does require some support from the data type facility. This post is getting a tad long so i'll write up some modelling examples and share them later today. :)

[goldfirere]

Just reading through the proposal and comments now. Several thoughts:

• You say that this proposal doesn't affect optimizations. Yet optimizations are done over Core. So: does this proposal not affect Core? That is, is this a surface-Haskell only change, with no internal verification that we've gotten it right? That violates somewhat the general design philosophy of Haskell, in that we verify GHC's implementation by type-checking Core. In addition, I would imagine that multiplicity information would be useful in optimizations, so there seems to be a lost opportunity here. EDIT: The end of the proposal elaborates on this, but I think this elaboration conflicts with the opening salvo.

• What is discouraged about using (:) in types? I'll likely fight against you on stealing this operator.

• It's unfortunate that there is no syntax for defining a record constructor with fields of varying multiplicity.

• Though the details are well beyond me, I've heard of instances where the expressions f and \x -> f x have different performance behavior. If we understand the former to mean the latter, will this affect performance? I also wonder if this affects sharing: If I say .... map f xs .... map f ys ... (where map is the plain old unannotated map from base), then do I allocate two closures for the fs? That would be unfortunate.

• Will a record constructor defined with GADT syntax also be linear in all its fields? I don't care very much about the answer, but it should be in the proposal.

• How will linear arrows interact with the reflection mechanism (i.e. Typeable)? I assume that a user of Typeable will be able to observe linearity, even if -XLinearTypes is not in effect.

• Unsurprisingly, the 0 multiplicity appeals to me. But, if you don't have a good story around it, then it makes sense to hold off. It doesn't seem like avoiding 0 for now will actually make it harder later.

[AshleyYakeley]

Same as above, should be x * 1 = x.

[aspiwack]

Indeed

• Fix this

[cartazio]

to build on @goldfirere 's point:
all the "multiplicity/usage" info is already on EVERY BINDER in core, or at least an approximating analysis for optimization purposes, and it'd be very easy to enrich that with the source / typing based sibling information. and at least internally at the core level something like what i've dubbed a linear function space (ie f :: usage0 (# :: usageA1 A1 , ... :: usageAn An #) -> (# :: usageB1 B1 , ... :: usageBm Bm #)) will be needed to give nice account of join points and direct applications vs partial applications semantically. (and I thusly would like exposed at the source level in some fasion that i can't currently see expressible in this proposal)

things i'd like to see this proposal address

1. Will adding this LinearTypes Proposal provide a tool that enables researchers (or industrial folks like ) to teach a functional programming flavor of full linear logic to our fellow scientists and engineers? (I'd want to see at least some way to do a simple emulation all the connectives from full classical linear logic in the proposed design)

2. being able to define/use nontrivial mixed usage datatype definitions. This is actually kinda important: for rich enough logicy applications, data types are how we, as PL influence computer scientists and engineers, model embedded domains/logics within our host tool.

what I can provide to help clarify my asks

1. some haskell / agda style data types that motivate interesting linear logical modelling opportunities once they get equipped/ enriched with usage/multiplicity information

[cartazio]

Callan: any pattern guard expression on a nontrivial data structure that’s linear will consume it. It gets consumed by the guard and then it can’t be used in the body. Dup in the desugaring is like “borrowing” in rust. But a semantics that actually allows tail calls and or bottoms.

…

On Fri, Feb 14, 2020 at 2:15 PM Callan McGill ***@***.***> wrote: @cartazio <https://github.com/cartazio> : Would you mind giving an explicit example for what could go wrong with pattern guards or where you envision needing a safe dup operation here? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#111?email_source=notifications&email_token=AAABBQS3W6WNINYHC2KVEUTRC3UV5A5CNFSM4EQO6C2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEL2DNCY#issuecomment-586430091>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQUWV2VXQYJ463INCR3RC3UV5ANCNFSM4EQO6C2A> .

[Boarders]

Just to check I am following, if I were to have the following code:

data Nat where
  Zero :: Nat
  Succ :: Nat .-> Nat

isEven :: Nat .-> Bool
isEven Zero     = True
isEven (Succ n) = not . isEven $ n

roundUpToEven :: (Nat .-> Nat)
roundUpToEven n | isEven n  = n
                | otherwise = Succ n

The claim is that because isEven consumes n we cannot then use it within the body of the function, is this correct? I haven't yet really dived into the proposal so far so apologies if this implementation is obviously deficient in some other respect, I just want to be clear on what exactly is being claimed.

[lexi-lambda]

That’s also true about ordinary guards, or plain if ... then ... else expressions, or case expressions on Bools. How is that at all surprising? Yes, linearity restricts what you can write; that’s the point.

I’m sorry, but this line of discussion is absurd. When you initially started complaining about this, you made some very serious claims, apparently believing this proposal was fundamentally flawed in some deep way. Now, a week later, the best explanation you can provide is a vague allusion to something wrong with pattern guards?

You posted your complaints on this proposal, on the libraries and ghc-devs mailing lists, on r/haskell, and on twitter. You’ve made an awful lot of noise for a quibble about technical minutia that belongs nowhere except as a comment (with concrete examples!) on this proposal. If you can’t back your (frankly rather insulting) claims up, then this incident is so unprofessional that I question whether your membership on the CLC is appropriate.

[cartazio]

@Boarders exactly! thanks for helping explicate. a desugaring from pattern guards into core's case would need to put a dup or split in front of the case (or after) and before the body rhs along with the with the guard.

[Bodigrim]

this incident is so unprofessional that I question whether your membership on the CLC is appropriate.

@lexi-lambda, with all due respect, it would be most professional to keep this discussion purely technical and refrain from personal attacks. It is already heated enough.

I do believe that whenever people raise questions (whatever stupid) or make claims (whatever bold), we should discuss their technical merits and not persons themselves or their membership in third-party organisations.

[davemenendez]

Callan: any pattern guard expression on a nontrivial data structure that’s linear will consume it. It gets consumed by the guard and then it can’t be used in the body.

Isn't this is the expected behavior of a linear type system? To preserve the linear use property, you would want T .-> (Bool, T) rather than T -> Bool.

Having some sort of convenience for using guards might be useful down the line, but that seems like a separate issue.

[cartazio]

Most systems people use allow some form of “borrow ” Or auto generated dupe to allow predicates. I’ll dig up references on the latter. I’m not sure if they’re written out in any thing aside from folk lore / private communications in this area. For vanilla ifs you can kinda do this rewriting partially by hand with an extra let to help out with the dupe , but pattern guards in pattern matching either via function definition or in case expressions basically would need to be hand desugared and these extra let’s between the case and the pattern guard predicates that check the rhs would be needed. Needing to manually desugar pattern guards to get nontrivial programs / libraries adapted to the extension seems like a huge amount of work. Pattern guards a very common / core part of Haskell programming. For those who want really meticulous rigorous expositions that spell out choices , is that’s gonna take some time to finish cause it’s not my day job, and my style of thinking requires my friendly collaborators to give me a good feedback look for what most folks consider clear and concrete. I tend to find abstraction concrete and concrete abstruse. So be patient. Everyone here wants nice things. It’s just we’re not agreeing on the path and consequences of choices to a goal. Not all of us have mutually compatible communication styles but have overlapping long term interests we aggressively care about but think about differently. Sometimes this can feel like conflict. But at the end we should always to assume good faith in the assumption that we all want a nice end state that makes our tools and ability to build great software / software tools I get very impassioned and aggressive sometimes around ideas and goals I care about. I like to think I’ve gotten more constructive about directing that in recent years. Likewise, people literally think differently. (Allegedly there are people who are unable to have an internal monologue of words without actually vocalizing their thoughts?!). I generally have a style of wholes systems thinking where I see a path to an end state and or the consequences of different paths , but it takes a long time for me to translate that into the communication styles that other folks digest easily. Which makes me really appreciate the folks with who I can collab with because then the whole process happens much much faster. For those who want me to explain and concretize some of my points in the ways they best engage with, I respect that but then you need to respect that it’s gonna happen In a time scale That isn’t some slap fight. The goal here is nice things and mutual education. And compiler patches. And examples. And maybe a cool paper or two. For fun or for professional reasons. Happily I have some lovely collaborators who wind up helping me translate These things into clearer forms.

…

On Fri, Feb 14, 2020 at 5:50 PM David Menendez ***@***.***> wrote: Callan: any pattern guard expression on a nontrivial data structure that’s linear will consume it. It gets consumed by the guard and then it can’t be used in the body. Isn't this is the expected behavior of a linear type system? To preserve the linear use property, you would want T .-> (Bool, T) rather than T -> Bool. Having some sort of convenience for using guards might be useful down the line, but that seems like a separate issue. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#111?email_source=notifications&email_token=AAABBQSBMR5NM6NLZJVCG6LRC4N4VA5CNFSM4EQO6C2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEL2WYNA#issuecomment-586509364>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQUOMK7AXON6SR4HJJDRC4N4VANCNFSM4EQO6C2A> .

[Tarmean]

I can give a good motivation for & types.

catchL :: (Exception e, l + r == 'One) => RIO a #l-> (e -> RIO (Unrestricted a)) #r-> RIO a

This forces the handler to free exactly the resources that occur as free variables in the action. It might free (or try to use) already freed resources but since they have to be tracked globally anyway it's simple to make that idempotent and raise a new exception respectively.
To deal with newly allocated resources in the action catchL needs to push a nested destructor map that is merged with the parent map when the action runs to completion.

I did actually try to make this work using the Either (a ->. k) (b ->. k) ->. k encoding before knowing that additive conjunction was a thing in linear logic. It's absolutely unusable as an api exposed to the end user.

More generally this sort of function type fills a similar role to laziness - it lets you write control flow as functions. Losing this capability in linear code really hurts usability in my experience.

[cartazio]

@Tarmean well said and thanks for saying it in your own words (better than I have tried in the past on this family of proposals)

theres also a realted issues that totally valid linear logical analogues of the maybe and either combinators are inexpressible in this proposal.

Exactly!  This is one example I was thinking of but explaining poorly.  Thank you for helping articulate this! 
And to do this efficiently needs this stuff to be natively representable. Which requires generalized join points. We have "1-arity &" via join points ,  traditional & is the 2arity case.  
N-join points , for N  >=0 upwards, give us an explicit syntax for 

• N=0 : syntax for casing on void and deriving absurd combinator from that.  

• N= 1  : what we call join points in haskell are essentially this

• N >= 2 : what you need for modelling exceptions that recover/manage/finalize resources at @Tarmean sketches above, OR writing linear logical analogues of the casing combinators such as either or maybe and their analogues for other sum types

[cartazio]

@monoidal #111 (comment) was the typing rule i mentioend a while ago for sketching out Choice/Generalized join points, will have to stare at it again to make sure its the correct one (it and other design feedbacks / discussions got lost in githubs "hide all the things")

[monoidal]

@cartazio

Currently, a join point is simply a let-in expression of a special form. If you'd like to have multiple branches, you use case, which shares the usage environment across branches. I see no reason to couple those two concepts into one. In particular, the fact that a case statement with two branches behaves like & in linear logic is not connected to join points (which are about avoiding allocation).

If I understand you correctly, you have an alternative vision and would like to change join points in Haskell to have more branches. Fine, but in that case please prepare a document with specific changes you'd like to make. The comment you have linked to is by your own admission not in a workable state ("fuzzy type rules", "are reachable patterns from a common type t? -- not sure about this side condition here", "will have to stare at it again to make sure its the correct one").

Perhaps, we could add codata declarations to Haskell in the future, and then we could have e.g. ifThenElse :: Bool #-> a & a #-> a. Or we could add a primitive & type with a special typing rule. The proposal is not blocking any of those ideas. However, this should be a separate discussion and a separate proposal. It's not possible to add linear codata if we don't have linear functions first.

[goldfirere]

I have merged this proposal, given that it is conditionally accepted (and has been for some time: #111 (comment)). All remaining conditions (now written in the proposal itself, so they are not lost) are implementation oriented and should not affect the text of the proposal.

Any changes one might want to present against this proposal should be in the form of a new PR, either as an amendment to this proposal or a fresh proposal.