New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Linear types #111

Open
wants to merge 62 commits into
base: master
from

Conversation

@aspiwack
Contributor

aspiwack commented Feb 13, 2018

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

This comment has been minimized.

cocreature commented Feb 13, 2018

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

This comment has been minimized.

Contributor

aspiwack commented Feb 13, 2018

@cocreature fixed. Thanks!

@Ericson2314

This comment has been minimized.

Ericson2314 commented Feb 13, 2018

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

This comment has been minimized.

Saagar-A commented Feb 13, 2018

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

This comment has been minimized.

cartazio commented Feb 14, 2018

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

This comment has been minimized.

gbaz commented Feb 14, 2018

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

This comment has been minimized.

cartazio commented Feb 14, 2018

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

This comment has been minimized.

cartazio commented Feb 14, 2018

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

This comment has been minimized.

cartazio commented Feb 14, 2018

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

@aspiwack aspiwack referenced this pull request Feb 15, 2018

Closed

Linear types #91

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Feb 15, 2018

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.

~~~~~~~~~~
We say that a function ``f`` is *linear* when ``f u`` is consumed
exactly once implies that ``u`` is *consumed exactly once* (defined

This comment has been minimized.

@AshleyYakeley

AshleyYakeley Feb 15, 2018

repetition of "consumed exactly once"

This comment has been minimized.

@aspiwack

aspiwack Feb 16, 2018

Contributor

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

This comment has been minimized.

@AshleyYakeley

AshleyYakeley Feb 16, 2018

NM, I misread it.

1 * x = x
x * 1 = 1
ω * ω = ω

This comment has been minimized.

@AshleyYakeley

AshleyYakeley Feb 15, 2018

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

This comment has been minimized.

@aspiwack

aspiwack Feb 16, 2018

Contributor

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

  • Fix this.
@cartazio

This comment has been minimized.

cartazio commented Feb 15, 2018

@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

This comment has been minimized.

Ericson2314 commented Feb 15, 2018

@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

This comment has been minimized.

Contributor

andrewthad commented Feb 16, 2018

@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 referenced this pull request in tweag/ghc-proposals Feb 16, 2018

@aspiwack

This comment has been minimized.

Contributor

aspiwack commented Feb 16, 2018

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

This comment has been minimized.

Contributor

andrewthad commented Feb 16, 2018

@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

This comment has been minimized.

cartazio commented Feb 16, 2018

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

This comment has been minimized.

cartazio commented Feb 16, 2018

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

screen shot 2018-02-16 at 11 04 40 am

screen shot 2018-02-16 at 11 04 57 am

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

This comment has been minimized.

Ericson2314 commented Feb 16, 2018

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

This comment has been minimized.

cartazio commented Feb 16, 2018

.... 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

This comment has been minimized.

cartazio commented Feb 16, 2018

@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

This comment has been minimized.

Contributor

goldfirere commented Feb 16, 2018

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.

0 * _ = 0
_ * 0 = 0
1 * x = x
x * 1 = 1

This comment has been minimized.

@AshleyYakeley

AshleyYakeley Feb 16, 2018

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

This comment has been minimized.

@aspiwack

aspiwack Feb 23, 2018

Contributor

Indeed

  • Fix this
@cartazio

This comment has been minimized.

cartazio commented Feb 17, 2018

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
@niobium0

This comment has been minimized.

niobium0 commented Oct 24, 2018

Syntax-wise I would like to float the idea of having f :: a ->{n} b ->{m} c.

IMHO for readability considerations it's important to have the -> on the left side of the multiplicity, because we read Haskell left to right, and the most essential quality of the linear arrow is that it's an arrow. Braces are not an ideal choice (potential complications in parser; records in types), but they seem to be better than underscores (i.e. f :: a ->_n b ->_m b) because of PartialTypeSignatures and NamedWildCards extensions.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Oct 25, 2018

Yes, I quite like braces.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 25, 2018

I like the braces too. How would this work with levity polymorphism? If we wanted to supply levity arguments explicitly, I suppose we would go into a prefix notation (->) @rep1 @rep2 @mult arg res)? (I've used visible kind application, https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-type-level-type-applications.rst, and whose implementation is nigh.) That is, the braces notation would be unavailable in prefix, but that's OK.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Oct 25, 2018

Polymorphism

map :: forall p a b. (a ->{p} b) -> [a] ->{p} [b]
@jeltsch

This comment has been minimized.

jeltsch commented Nov 8, 2018

After the semantics of this proposal have been settled, I was hoping to have a very little discussion on the name of the language extension, and whether it could be changed to something like -XLinearArrows or -XLinearFunctions; instead of -XLinearTypes.

-XLinearArrows would be bad, since an arrow in the Haskell sense is an instance of the arrow class. -XLinearFunctions sounds good.

@cartazio

This comment has been minimized.

cartazio commented Nov 8, 2018

@jeltsch

This comment has been minimized.

jeltsch commented Nov 9, 2018

That’s an argument. So better call the extension LinearFunctionTypes or simply stick to LinearTypes.

@jeltsch

This comment has been minimized.

jeltsch commented Nov 9, 2018

The proposal currently says that each data constructor has two different types: one when used as a constructor function and one when used in pattern matching. This is a phenomenon that, to my knowledge, doesn’t exist anywhere else in the language and that makes understanding data constructors difficult.

I also believe this feature will lead to unsoundness once we add the 0-multiplicity, since for example (:) will also have type a # 0 -> [a] # 0 -> [a] then, which is clearly wrong.

Would it be possible to give data constructors a single type, namely the one without multiplicity, and use slightly different typing rules in code where LinearTypes is not enabled to achieve compatibility?

@jeltsch

This comment has been minimized.

jeltsch commented Nov 9, 2018

I propose to change the multiplicity name Omega to something better, for the following reasons:

  1. It’s already questionable that the paper uses the symbol ω. The choice of this symbol stems from its use for the smallest transfinite ordinal number, the number that denotes the length of an infinite list, if you so wish. This doesn’t match the use of ω in this proposal, where it stands for the possibility to use a value any number of times and thus rather corresponds to something like ℕ ∪ {ω}.

  2. Even if ω is considered okay for being used in the theory, we shouldn’t use the identifier Omega in Haskell. Omega doesn’t name the multiplicity; instead it names the symbol that is used to denote the multiplicity.

  3. To people not into something like ordinal numbers or ω-words, Omega doesn’t mean anything. Therefore its use would rather confuse than enlight those people.

I propose to pick multiplicity identifiers that capture the actual meanings of the multiplicities and are consistent with existing identifiers at the same time. Control.Applicative already uses the identifiers some, many, and optional. We could use Many for what is now called Omega and Optional for the affinity multiplicity in case it’s added at some time. I think One is a good name and thus should be kept. The 0-multiplicity would probably be best named None.

@jeltsch

This comment has been minimized.

jeltsch commented Nov 9, 2018

I’m a bit concerned that we might end up with a syntax that will lead to problems with readability or comprehensibility. I think it’s important to address the issue of syntax soon, since any syntax that will make it into a stable GHC version is likely to stay forever.

I strongly recommend to adopt the #-syntax proposed by @davemenendez, which is mentioned as an alternative in the proposal. In this syntax, function types with multiplicity parameters are written a # p -> b (where p is the multiplicity) and λ-expressions are written \ (x :: a # p) -> e or simply \ (x # p) -> e. Note that the intention is to put spaces around multiplicities; the goal is not to construct an arrow that looks like #p-> (as the description in the proposal might suggest).

In the following, I’ll argue why I think this notation is the best we have. In transit I’ll mention shortcomings of other choices, some of them very serious in my opinion. Not all of my arguments are new, but I think it’s good to have all arguments listed in one place.

  1. The notation for function types, a # p -> b, makes it clear that the multiplicity parameter p denotes the multiplicity of the domain. The notation a ->{p} b, on the other hand, might suggest that p denotes the multiplicity of the codomain. In the best case, it suggests that p belongs to the ->. Of course, p is a parameter of the function type and thus technically does belong to the ->, but morally it belongs to the domain only.

  2. The #-syntax is readable. In contrast, notations that try to construct specific arrows by mixing symbols with multiplicity parameters make reading hard and at the same time don’t achieve their goals. For example, :p-> makes it difficult to recognize the p as a separate construct that carries a meaning and at the same time doesn’t really look like an arrow.

    Readability gets worse when the multiplicity isn’t given by a single identifier anymore. Consider the following example, where the multiplicity is just a simple application:

    f :: Int :(F a)-> a -> a
    

    It’s even hard to recognize the F a as a unit. We are used to subconsciously splitting Haskell constructs at whitespace and thus are likely to consider :(F and a)-> units rather than F a. The #-variant is much more legible:

    f :: Int # F a -> a -> a
    

    What helps here is the fact that Int # F a looks to a Haskeller like an application of an infix operator. While this perception is technically wrong, it still conveys the idea that the Int and the F a belong together, which they do.

    Similar considerations apply to the notation for patterns. For example, x ::(F a) b suffers from the same problem as the above example with :(F a)->, while x :: b # F a is legible.

  3. The #-syntax is consistent. No matter whether you have a function type or a pattern, you always write # p to state the multiplicity. On the other hand, the syntax used in the proposal uses different notations for attaching multiplicities (:p in the case of functions, (p) in the case of patterns). Other proposals suffer from the same problem.

  4. The #-syntax doesn’t force you to provide a type annotation in patterns with multiplicities. You can just write \ (x # p) -> e instead of \ (x :: a # p) -> e. Other syntax proposals attach the multiplicity to the :: and thus require you to provide a type signature.

  5. The #-syntax naturally extends to constructs other than function types and patterns:

    • We can have case expressions with explicit multiplicities like in the paper, using the notation case e # p of ....

    • We can have multiplicity annotations in ordinary (non-GADT) data type definitions. For example, Unrestricted can be defined as follows:

      data Unrestricted a = Unrestricted (a # Many)
      
    • The notation x :: a # p can be used for declaring record fields with multiplicity annotations.

    • If linear top-level variables should be introduced at some point, we would have a notation for specifying their multiplicities that is consistent with the other notations: if a type signature x :: a is present, it would be extended to x :: a # p; if no type signature is present, a “multiplicity signature” x # p would be added.

Using # for specifying multiplicities steals syntax, as it makes it impossible to use # as an operator on types. However, MagicHash already restricts the use of # as an operator; so people are probably already reluctant to name their operators #.

To avoid stealing syntax, we could use | instead of #, as @goldfirere suggested. However, this would introduce a clash with existing syntax in the case of bindings, where the p in a binding x | p = e could be a multiplicity or a condition. Furthermore, the use of | might result in slightly confusing code when patterns with multiplicities occur close to guards, as in the following example:

f (x | One) | x > 0     = True
            | otherwise = False
@cartazio

This comment has been minimized.

cartazio commented Nov 9, 2018

@bravit bravit added the Proposal label Nov 11, 2018

@jberryman

This comment has been minimized.

jberryman commented Nov 12, 2018

I'm very new to this proposal, having only watched simonpj's talk here last week, and currently studying this version of the proposal and comments here as best I can, so I'm not sure how helpful these comments and questions will be. Maybe it will be helpful in preparing to introduce and explain the feature to the community.

unrestricted seems weird

My primary hang-up is unfortunately quite early on, and I think it boils down to the exact meaning of "unrestricted" and the One/Omega distinction. Maybe it would be simplest to approach this by explaining how I imagine (in my ignorance) LinearTypes should work, and certain implications:

  • f :: A -> B -> C says nothing about the multiplicity of the arrows in f; we've omitted the "multiplicity signature" and GHC infers it for us, just as GHC infers a type (that we can inspect in ghci, etc) when we omit a normal type signature

  • Within a multiplicity signature we can have

    • which means the LHS is consumed exactly once,
    • -many-> (or whatever) which means non-linearity, i.e. the argument may (at runtime, in some branch) be consumed more than once (or not at all?),
    • or a multiplicity-polymorphic arrow
  • It follows (I think) that polymorphism in a multiplicity signature may occur only in higher-order functions (insert something more precise re. positve/negative position args), and those arrows originate in the argument functions: GHC infers monomorphic (non-)linearity for all the code in a function f's body (and checks it against the multiplicity signature, if provided), while functions passed in as arguments to f are inferred to have mult-polymorphic arrows (if not constrained by a signature) These arrows may show up further to the right in the top-level signature of f, depending on how the argument functions are called, etc.

NOTE: The "multiplicity signature" is just an organizing concept I find helpful, and need not be syntactically an actual separate signature. This is more about the meaning of ->.

To riff more on this: in @simonpj's talk referenced above, he gives the problem of:

f :: Int -o Int
g :: (Int -> Int) -> Bool
g f -- OOPS ill-typed!

And presents the solution as making f mult-polymorphic, as in f :: Int ->ₚ Int. But it seems to me this should (without even inspecting the body of f) be some sort of "rigid multiplicity" error; that is in f the compiler knows whether the argument to f is consumed once, many times, or not at all. The error being analogous to:

f :: Ord a=> a -- OOPS! rigid type error
f = 'x'

In the actual proposal it seems the meaning of "unrestricted"/omega means "we won't (even though we could?) say anything about how the LHS is used", but it's actually not terribly clear to me.

If my understanding is correct, I find it a confusing notion (the omega arrow already seems per se like a polymorphic thingy, yet it doesn't unify with lollipop...). It seems like replacing it with the Not-Linear Arrow and treating multiplicity annotations like a separate (possibly omitted) signature (even if syntactically they were fancy arrows in the normal type sig) has some benefits, e.g.:

  • only people writing libraries that make use LinearTypes in their APIs need to write multiplicity-signatures
  • base etc don't need to be rewritten, new GHC just infers multiplicity (this seems like a big deal)

To be honest I'm not sure the degree to which what I've described differs from the proposal as written (though I think it's significant, e.g. currently mult-polymorphism is never inferred). I don't follow the discussions of inference, but I assume that the compiler must be able to infer "this function is linear" (i.e. surely everything doesn't hinge on trusting programmers when they type a lollipop in a signature).

I think it's likely this has been hashed out before and dismissed for good reasons, but maybe the proposal or future pedagogy could expand on what "unrestricted" means. Or it might be helpful for others to understand why the notion of "unrestricted" was chosen over "not-linear".


Other ideas / questions

  • I don't really understand the GADT data decl syntax. Is the intention there just to be able to specify what it means for a value of that type to be "consumed exactly once"? If so is reusing the arrow syntax really appropriate? It seems like a kind of punning that just confuses things, but I'm probably missing something
  • the proposal talks about both "multiplicity of binders" and "multiplicity of functions", so what does multiplicity actually mean? It seems to me you have to talk about multiplicity wrt the arrow, (EDIT: I think I'm being pedantic). The "binder multiplicity" syntax in 2.3 seems like just more stuff to learn and parse when reading new code
  • ...however I think I like the syntax suggestions by @jeltsch (I certainly like the philosophy of stepping back and thinking of syntax that reflects an intuitive mental model for the average haskell programmer).

Thanks to folks at Tweag all who have worked so hard on this proposal!

@davemenendez

This comment has been minimized.

davemenendez commented Nov 12, 2018

I agree with @jeltsch that Omega is not a great name for the unrestricted multiplicity. It's perfectly understandable for people who are familiar with the underlying theory, but I'd rather have something that provides a clue for everything else. (See also pi vs foreach in the dependent Haskell discussion.) Many is better, since it gets across the idea of "more than one", but in common usage "many" never means "zero" so it isn't perfect. Something like Unlimited or Unrestricted get across the right meaning, but they are possibly too broad. ZeroOrMore has the right meaning and scope, but is a bit clunky.

(I also agree with @jeltsch about the # syntax. Thanks for making an explicit argument, which I kind of forgot to do.)

@int-index

This comment has been minimized.

Contributor

int-index commented Nov 12, 2018

I'm against the # syntax. Please, pick a symbol that doesn't conflict with -XTypeOperators (or any syntax present in terms), – unifying term/type parsers is enough of a headache as it is. It would be a step back after #143

@davemenendez

This comment has been minimized.

davemenendez commented Nov 12, 2018

@jberryman Regarding multiplicities: yes, logically A ->. B (or A # One -> B) is a subtype ofA -> B (or A # ZeroOrMore -> B), but type inference and subtypes do not go well together. This leads to the problem you mention where using some higher-order functions becomes trickier.

The meaning of Omega (or ZeroOrMore or whatever) isn't so much "non-linear" as "not known to be linear". So it's always okay to "forget" that a function uses its argument exactly once. In that sense, the types A ->. B and A # p -> B are the same (although we'd have to exclude Zero if it becomes part of the system).

In the higher-order case, g :: (A -> B) -> C means that g wants a function that isn't known to be linear, so we can't write g f unless we forget that f is linear (e.g., by writing g (\x -> f x)). Since we can always forget that a function is linear, we could have written g :: (A # p -> B) -> C and gotten the same meaning.

However, I think the trend will be to only use multiplicity polymorphism for higher-order functions where the overall multiplicity depends on the multiplicities of their function arguments, such as map :: (a # p -> b) -> [a] # p -> b. I think it would be possible to convert g to have the weaker type shown above without a run-time cost, but I haven't worked out the details.

@jeltsch

This comment has been minimized.

jeltsch commented Nov 12, 2018

I agree with @jeltsch that Omega is not a great name for the unrestricted multiplicity. […] Many is better, since it gets across the idea of “more than one”, but in common usage “many” never means “zero” so it isn’t perfect.

I agree with this. Actually, “many” doesn’t even include “one” in common usage. However, many is already used to mean “arbitrarily many” (including zero and one) in Control.Applicative. So we already have that imprecision in the standard libraries, and using Many for what the paper calls ω would at least give us consistency, which is also important. Besides, Many is a catchy name. 🙂

@jeltsch

This comment has been minimized.

jeltsch commented Nov 12, 2018

I’m against the #-syntax. Please, pick a symbol that doesn’t conflict with -XTypeOperators (or any syntax present in terms); unifying term/type parsers is enough of a headache as it is. It would be a step back after #143.

What I call “the #-syntax” actually consists of two things: (1) the general approach of using notation of the form a ⟨symbol⟩ p -> b and x :: a ⟨symbol⟩ p and (2) the choice of symbol. I’m strongly advocating (1), but I’m much lesser advocating (2), although I think # is a good choice.

While I understand your concerns, I want to stress that they affect only (2). On the other hand, all 5 arguments listed in my above comment are arguments in favor of (1). Thus they are also arguments in favor of using the described notation with a different symbol as long as the choice of symbol doesn’t lead to conflicts with other syntax.

Personally I think we shouldn’t try to avoid stealing syntax at all costs. Stealing a little bit of syntax might be better than ending up with bad syntax for the new constructs. Currently Haskell operators can be virtually anything that isn’t used for other purposes in Haskell 2010. As a consequence, it’s almost impossible to extend Haskell 2010 with new symbolic syntax and not steal any possible operators at the same time.

Given that the use of # as an operator is already restricted by MagicHash, it might be a reasonable idea to disallow a single # as an operator altogether. This would remove any hurdle for unifying the term and type parsers.

However, even if you don’t agree with these opinions about #, please keep in mind that my comment is 99 % about something else: the notations a ⟨symbol⟩ p -> b and x :: a ⟨symbol⟩ p.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Nov 12, 2018

Personally I think we shouldn’t try to avoid stealing syntax at all costs. Stealing a little bit of syntax might be better than ending up with bad syntax for the new constructs.

I agree. I'm OK with stealing some syntax, for a good reason. Even better is when you can mitigate the fallout, as we can here: despite the fact that # would be magical here, it seems entirely sensible to import/export it from modules and to use it qualified. It doesn't require special parsing (it parses like an operator that binds just tighter than ->). At some point in the compilation pipeline (likely the renamer, when it rejigs parse trees to reflect fixities), the a # p -> b syntax gets transmogrified into some new node in the AST. So I think this is quite reasonable.

I also agree with @int-index that we want future syntax to work in both terms and types, but I think this one does. Note that the idea steals term-level syntax and type-level syntax, so both are on the same footing.

@int-index

This comment has been minimized.

Contributor

int-index commented Nov 12, 2018

Note that the idea steals term-level syntax and type-level syntax, so both are on the same footing.

I'm not sure, does it? This is actually my primary concern - will the treatment of # be exactly the same in terms and in types?

There seem to be two constructs that use it so far:

f :: a # p -> b

\(x :: a # p) -> ...

Both are in types.

Are we now certain that we're also looking to add these two?

case x # p of ...

\(x # p) -> ...

That would also steal from expressions and patterns, and then I'd be OK with this.

However, I still think # has enough existing uses (it's both an operator and syntax for overloaded labels). I'd rather pick something new, e.g. |#. This seems to work just as well.

@jeltsch

This comment has been minimized.

jeltsch commented Nov 12, 2018

@int-index

I think it’s not yet certain that we’ll have case x # p of ... and \ (x # p) -> ..., but it’s likely that we’ll want to add them at some point (especially the second one).

While I still think # would be a good choice, I’d find |# to be a sensible alternative in case the #-option shouldn’t make it.

@int-index

This comment has been minimized.

Contributor

int-index commented Nov 12, 2018

I’d find |# to be a sensible alternative

That's good to hear. Here are the benefits that I see:

  • We're not stealing any syntax.
  • The implementation will be more straightforward: a dedicated lexeme instead of magic in the renamer.
  • Error messages will be better: we can suggest to turn on -XLinearTypes if the user writes |# somewhere in the program.
  • The mental overhead will be smaller: I can immediately know what |# means without inspecting enabled extensions or current scope

That said, I'll be fine with another choice of syntax that doesn't steal existing syntax and behaves consistently across types, expressions, and patterns. |# just seems to fit that role well enough.

@jeltsch

This comment has been minimized.

jeltsch commented Nov 12, 2018

Actually, we do steal syntax when using |# for multiplicity annotations. The vertical bar is not a reserved symbol like, for example, ( and ); only the token the consists of a single | is reserved. Otherwise we couldn’t have an operator ||. So currently |# is a valid operator.

This is rather a case in favor of using #. Both # and |# are valid operators currently, but the use of # is already restricted by extensions like MagicHash.

@jberryman

This comment has been minimized.

jberryman commented Nov 12, 2018

@davemenendez Thanks. What you've described is what I thought I understood about the proposal. I guess my comment was too long-winded, but I was asking: why the particular formulation of One/ZeroOrMore proposed here and not One/Many? The former (with its logical subtyping relationship, with polymorphism over forgetfulness of a static property of the code...?) is quite confusing to me.

@int-index

This comment has been minimized.

Contributor

int-index commented Nov 12, 2018

Actually, we do steal syntax when using |# for multiplicity annotations. Both # and |# are valid operators

Silly me! Yes, this invalidates the |# idea. Forget I mentioned it. So now my only concern is that we have the same treatment in types/expressions/patterns for whatever symbol we steal.

@davemenendez

This comment has been minimized.

davemenendez commented Nov 12, 2018

@jberryman

I was asking: why the particular formulation of One/ZeroOrMore proposed here and not One/Many? The former (with its logical subtyping relationship, with polymorphism over forgetfulness of a static property of the code...?) is quite confusing to me.

Let's say I have a function,

foo :: Bool ->. Int -> Int
foo True  a = a
foo False a = 0

foo will use its second argument one or zero times, depending on its first argument. So, foo True is going to have the type Int -> Int even though it uses its argument exactly once. That's why I was describing One as "known to be used exactly once" and ZeroOrMore as "not known to be used exactly once."

There are also reasons why I might want to describe a linear function as non-linear, such as preventing it from being called by other linear functions.

@jberryman

This comment has been minimized.

jberryman commented Nov 13, 2018

@davemenendez

That's why I was describing One as "known to be used exactly once" and ZeroOrMore as "not known to be used exactly once."

Sorry, maybe I should have said "why One/ZeroOrMore and not One/NotProvablyOne?", i.e. it's the subtyping relationship that bothers me: it seems to me an arrow is either linear or not (this is a static property; "linear" means the property holds in every branch, else non-linear). The fact that there might be a branch that in isolation has the linear property, doesn't imply we need arrows with this kind of subtyping relationship.

You describe the proposal's omega arrow as "not known to be used exactly once", but afaict it actually means "I'm not telling" (maybe "I'm not telling" was chosen as part of the compatibility story?). There is missing a proper non-linear arrow. Restating from my original comment I wonder why there isn't:

  • -> = I'm omitting multiplicity annotation, infer it (EDIT: i.e. one of the three arrow flavors below) from the code body
  • -linear-> = the LHS is consumed once
  • -not-linear-> = not linear (i.e. there's some branch where LHS is not consumed exactly once)
  • ->p = multiplicity polymorphic (EDIT: either -linear-> or -not-linear->)

It seems to me it should always be a type error to twiddle a -linear-> to a -non-linear-> in a valid checked signature. In contrast it's always okay under the proposal to change ->. to the unrestricted arrow (spelled "->").

There are also reasons why I might want to describe a linear function as non-linear, such as preventing it from being called by other linear functions.

Hm, it seems like you ought to be able to solve that problem using types differently in your API in some boring way, but I haven't tried to design an API using linear types yet.

@davemenendez

This comment has been minimized.

davemenendez commented Nov 13, 2018

@jberryman

Sorry, maybe I should have said "why One/ZeroOrMore and not One/NotProvablyOne?", i.e. it's the subtyping relationship that bothers me: it seems to me an arrow is either linear or not (this is a static property; "linear" means the property holds in every branch, else non-linear). The fact that there might be a branch that in isolation has the linear property, doesn't imply we need arrows with this kind of subtyping relationship.

We can think of it in other ways. If I have f :: A ->. B, then f is guaranteed to use its argument exactly once, while g :: A -> B makes no guarantee. I'm always free to ignore/discard/weaken a guarantee, so I can turn f into (\x -> f x) :: A -> B. If I couldn't do that, then I would not be able to do things like create the list [\x -> f x, g].

You seem to be arguing that the guarantee should always be as strong as possible (i.e., if the list contains no non-linear functions, then it must have the type [A ->. B]). This seems akin to saying that const :: a -> a -> a is ill-typed because it could be made more general. I can always make a type less polymorphic, so why can't I weaken a linearity guarantee?

Now, we could add additional multiplicities such as NotOne or MoreThanOne, which would guarantee non-linear use. Converting f :: A ->. B to the type A # NotOne -> B would be impossible, because One is not weaker or stronger than NotOne. We would still need ZeroOrMore, though, in order to handle situations where no guarantee is possible.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Nov 13, 2018

@davemenendez's recent example makes me wonder about this:

data SBool :: Bool -> Type where
  STrue :: SBool True
  SFalse :: SBool False

type family If b t f where  -- in Data.Type.Bool
  If True t _ = t
  If False _ f = f

dep :: SBool b -> Int :(If b One Omega)-> Int
dep STrue x = x
dep SFalse _ = 0

The theory appears to like it. Will the implementation?

@jberryman

This comment has been minimized.

jberryman commented Nov 13, 2018

@davemenendez I appreciate your responses. I think I'm understanding the reasoning behind the approach much better now.

If I couldn't do that, then I would not be able to do things like create the list [\x -> f x, g] ...... You seem to be arguing that the guarantee should always be as strong as possible (i.e., if the list contains no non-linear functions, then it must have the type [A ->. B])

This was a really helpful example. So I'm coming to this proposal from the opposite direction actually: linearity is a property of functions (right now, in current haskell). This property actually propagates in a particular way as functions are composed (taking your example: foldr1 (.) [f, g] is linear iff both f and g are linear).

So my difficulty with the proposal was I expected the actual linearity properties of code to be inferred and propagated (just as I could reason about linearity if all the RHSs were available to inspect) in the type system. But I see now that this is really difficult (e.g. as you say, what is the type of [f, g]?). So IIUC the Hard Problem the proposal solves is how to shoehorn some linearity information into the existing type system, rather than I suppose inventing some brand new "multiplicity system" or something.

Appreciate it, and won't drag discussion further OT!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment