Sugar for linear arrows

[Lysxia]

Linearity seems ubiquitous enough that it would be useful to have special syntax for it.

A #-> B
-- as sugar for
(1 _ : A) -> B

In particular that allows you to easily make an existing module use linear types by search-replace; in vim: :s/->/#->/gc.

[andrevidela]

I've been thinking about that a lot lately and even when through partially implementing an alternative syntax for linear arguments. But I think we should hold off on this feature request for the following reasons.

1. There is no support for 0

While linearity happens more often than erased types, it would still be very weird to have a syntactic asymmetry between linear and erased arguments. Why would linearity get special treatment when those examples still happen:

interface Functor (f : (0 _ : Type) -> Type) where
    ...

I understand that erased annotation do not appear as often as linear ones, but this specific example leads me very well into the next one: Linear interfaces could use some linear polymorphism, actually a lot of Idris would benefit from linearity polymorphism, which leads me to point 2.

2. There is no upgrade path towards polymorphic multiplicities

In the future it would be nice if we could do that

map : forall l . (f : (l v : a) -> b) -> (l xs : List a) -> List b
map f [] = []
map f (x :: xs) = f x :: map f xs

while it would make today's implementation nicer, it is not obvious how to go from

map : (f : a #-> b) -> List a #-> List b

to

map : forall l . (f : (l _ : a) -> b) -> (l _ : List a) -> List b

3. There is no upgrade path to alternative quantity semirings

One thing that would be useful to have is to allow our program to make use of more complex quantities like Nat instead of 0, 1, ω. In this semiring, 1 does not have any special meaning beside the fact that it's the neutral for multiplication (which only happens behind the scenes). As a matter of fact, the compiler already has partial support for interpreting alternative semirings. Given this, there is no reason to give a special syntax to 1

drop : (0 _ : a) -> ()
drop _ = ()

copy : (2 _ : a) -> (a, a)
copy a = (a, a)

id : (1 _ : a) -> a
id a = a

This example would lose the nice syntactic symmetry if the identity has a different syntax.

4. There is no upgrade path to dependent linearity

This is getting a bit far fetched, but maybe not: It would be nice if quantities were values in the language themselves and could depend on other values (given some limitations). for example imagine the map function on vectors which explicitly states that the higher order function will be called exactly n times.

map : {0 a, b : Type} -> {0 n : Nat} -> {0 l : Rig} -> (n f : (l v : a) -> b) -> (l _ : Vect n a) -> Vect n b

This is particularly useful if you want to get a solid hold on memory usage depending on usage variables. In the following example we allocate a vector using n copies of a variable that will get accessed n times.

replicate : (n : Nat) -> (n val : Lazy a) -> Vect n a

5. Alternative solutions

There actually are other proposals that would be less intrusive and would allow an easier upgrade path toward the future developement of Idris2:

Language pragma

Start your file with

%linearity linear

This option could be extended with other arguments like

%linearity finite

which wouldn't allow ω as a linearity

or

%linearity erased

which would make everything linearity 0 by default

Function annotation

Similar but more fine-grained: Allow to annotate functions with a flag that tells the compiler to automatically assume arugments are linear instead of unrestricted when not annotated

linear
plus : Nat -> Nat -> Nat
plus Z m = m
plus (S n) m = S (plus n m)

Again this could be extended to support other flags like

linear polymorphic
plus : Nat -> Nat -> Nat
plus Z m = m
plus (S n) m = S (plus n m)

Which would avoid the forall ceremony.

Compiler flag

One could imagine having a special compiler flag for a restricted subset of idris that only accepts linear or bounded linear annotations. Calling the compiler with --graded would enable its more where arbitrary finite semirings are allowed and aggressive memory management optimisations are performed.

Conclusion

I understand you intention and I'm happy this discussion is happening but I would advise against syntax changes related to linearity for now since the feature is still missing some key insight into how it is being used, and how it should be used. As far as I know there are maybe 3 or 4 large projects written with Idris2 and they are not even all using linearity, and not in ways we necessarily expect. I know it's tempting to simplify our lives with a nicer syntax but, as a research project, it seems counter productive to prioritise convenience over innovation. Though (again, as a research project) we don't mind breaking changes either, avoiding them is far easier. And in this case we have a very easy way to avoid future breaking changes: just don't implement special syntax for something that we have very little experience with.

Finally I would like to stress that the language is already weird enough for normal people without fancy syntax sugar, if a linear arrow were to be introduced I would suggest something that is already an industry standard in order to maximise familiarity, something like the lollipop -o arrow.

[Lysxia]

Thanks for the reply. I totally understand that it might be too early to commit to such syntax. I'm not going to push it.

Nonetheless let me mention that this syntax comes straight from the Linear Haskell extension, where I believe they have already thought through the upgrade path (addressing your points 1 to 4 which all have in common the need to generalize the syntax to other multiplicities than 1), which is to put the multiplicity between # and ->:

#1->  -- abbreviated as #->
#0->
#n->

The proposal for linear types in Haskell and its extensive discussion are public. Do not take this at face value. I'm not saying this is proof that this is the right syntax. And I'm not requiring anyone to read this 400-comment-long thread. But if someone feels strongly enough to carry on this discussion, I'm sure many of the points made there (both pros and cons) would carry over to Idris.

[andrevidela]

Ah that looks great actually!

[Lysxia]

Also, we can simply define #-> as an operator. We can have fixed-multiplicity arrows without changing the parser:

infixr 90 #->
a #-> b = (1 _ : a) -> b

It's generalizing that syntax that requires more work. There are really two ideas here, the second subsumes the first:

1. Add #-> (and maybe another one for 0) as an operator in the standard library
2. Change the syntax (1 _ : a) -> b to actually be something like #1-> in the first place, since having both seems redundant

(2) is a pretty big change, but as I mentioned earlier, (1 _ : a) -> b makes it a little inconvenient to make many arrows linear.

Example:

-- not linear
a -> (a -> b) -> b

-- linear, current
(1 x : a) -> (1 f : (1 y : a) -> b) -> b

-- linear, this proposal
a #-> (a #-> b) #-> b

I also tried using another operator for multiplicity 0, and ran into the small issue that = is non-associative:

-- not linear
x = y -> v

-- 0, current
(0 p : x = y) -> v

-- 0, this proposal (as an operator)
(x = y) ?-> v

-- 0, this proposal (change syntax)
x = y #0-> v

[ShinKage]

I think that for consistency, both with this new syntax and the with the current way of representing unrestricted value, the syntax should always be #(multiplicity)-> even for the linear case (so the only allowed way would be #1->), since not having an explicity multiplicity is currenlty translated to unrestricted.

Having both syntax should be fine, this new operator should be syntactic sugar not the regular representation, like with => for autoimplicits that really are just {auto _ : t} ->.

Due to the fact that the arrow -> is not really an operator, i think that also #-> should be treated in the same manner, to replicate the current interplay with other operators (as you discovered with the =).

[Russoul]

I don't know, (0 _ : a) -> b looks better to me than a 0#-> b.
4 symbols for an operator that is expected to be used much is just too heavy.
But that's just my opinion.

But a unicode variant would be actually cool !
⊸ (lollipop arrow) like in haskell for linear binders
We can invent one (if not already) for erased binders too

But I know unicode symbols in lexemes of the language is a controversial topic.
Linking Idris2-boot RFC
But at least maybe we could use well known unicode symbols like lollipop arrow.

Also I think entering unicode symbols should not be an issue in decent enough editors.
For example Vim has digraphs which basically allows
you to substitute a unicode character for a combination of two ascii characters

EDIT: I just thought about other issues Unicode could pose. The fact that Unicode lollipop arrow is one character wide and most fonts try to keep width of most, if not all, symbols same results in quite flattened rendering of it.

Now I believe the best middle ground solution would be to use -o for linear binders as @andrevidela mentioned:

• not heavy on eyes

• recognizable

• not far-fetched

• easy to implement

• integrates well with other quantity semirings (since 1 is one of the two neutral elements of any semiring)

[gallais]

I really like the a -o b (& (x : a) -o b for the dependent variant)
proposal for the linear implication. The original proposal (or something
along the same lines) is worth keeping for arbitrary quantities though.

[joelberkeley]

I'm having similar issues with unresricted quantities. Currrently, the default quantity is 0 and the only available sugar for specifying implicits (forall n .) is also for quantity 0. I'd really like more ergonomics for {n : _} ->.

[gallais]

Note that we have -@ in Data.Linear.Notation.
It only works for non-dependent linear arrows.