@-Patterns forcing bound implicit types to linearity 0

[donovancrichton]

@-Patterns on cases where implicits are introduced into scope automatically bring them as Linearity 0 on the right hand side.

Steps to Reproduce

Take the following definition of an ordinary cons-list where we specifically want 'don't care' linearity:

data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

and the following function:

g : MyList a -> ()
g [] = ()
g l@(x :: xs) = ?hole

Expected Behavior

:t hole
   a : Type
   x : a
   xs : MyList a
   l : MyList a
-------------------------------------

Observed Behavior

:t hole
 0 a : Type
   x : a
   xs : MyList a
   l : MyList a
-------------------------------------

A minimal example showing this can be found here: https://gist.github.com/donovancrichton/d0aa7aabeb83f918abc8037120c2222a

[gallais]

One problem I can see: what should the multiplicity of the as-pattern be when the variable is linear?

For zero and unlimited, we can pick zero & unlimited. Otherwise should we also default to zero? Or try something more subtle: if it's not bound in a user-written argument then one else zero?

[donovancrichton]

I'm not very across the subtleties of linear types yet to be honest, so please bear with me while I clarify my understanding (and please point out anything I get wrong!) :) As I understand it we have the following:

• Linearity 0 means we cannot match on the type. So we cannot use this on the LHS or the RHS.
• Linearity 1 means we must match on the type(?). We must use this on the RHS.
• Linearity Infinity means we may or may not match on the type, and we may or may not use this on the RHS.

Let if me know if I got this right to start with, and then we can think about where to go from here. :)

[andrevidela]

I think you got it but just for completeness here is what's going on with linearity 1

There are two modes:

1. Match on the constructor and use any variables bound by the matching on the rhs
2. Do not match but use the bound variable on the rhs

Here is an example of the first case

incNotZero : (1 _ : Nat) -> Nat
incNotZero Z = Z -- no values bound, nothing to use
incNotZero (S n) = S (S n) -- we bind the predecessor to `n` so it must be used

Here is an example of the second case

increment : (1 _ : Nat) -> Nat
increment n = S n -- we don't match but we bind `n` so it must be used

Here is an example mixing the two

plus : (1 a, b : Nat) -> Nat
plus Z n = n -- `n` isn't matched but is bound so we must use it on the rhs
plus (S n) m = S (plus n m) -- n is the result of a match and m isn't, both of them are linearly bound and must be used once

Finally another subtlety, linearity 0 doesn't necessarily mean forbidden use in all cases. You can use them for proofs on the rhs. That is, you can use them inside a rewrite or inside a function that expects an argument with linearity 0. Another way to see it is "forbidden use at runtime" and "unrestricted use at compile time"

[ziman]

Here are some counterexamples to what (I think that) you say, which should hopefully illustrate some of the possibly unexpected consequences of the rules. Descriptions are below each code snippet.

-- counterexample to "cannot match on the LHS"
-- matching on a zero-quantified argument
f1_subst : (0 eq : m = n) -> Vect m Int -> Vect n Int
f1_subst Refl xs = xs

Idris lets you match on an erased argument if it's the only constructor in the type family so its tag is forced, and all its fields are either forced, unused on the RHS, or used in erased positions on the RHS.

-- this is not really a match because the pattern is forced
-- you just can't see that in the source so it looks like you're matching on it
f1_isEmpty : (0 n : Nat) -> Vect n Int -> Bool
f1_isEmpty Z [] = True
f1_isEmpty (S n) ((::) {len = n} x xs) = False

This was meant to illustrate that you can see code that looks like it matches on an erased argument but, depending on the exact elaboration, it probably does not. Instead, the erased argument is forced to S n, where n is taken from the (::) constructor of Vect. Variable n happens to be erased, too, but that's not interesting here).

-- counterexample to "cannot use this on the RHS"
-- here you use 0-quantified `n` on the RHS
-- doesn't matter if it comes from the `Nat` or from the vector, both are erased
f1_vlen : (0 n : Nat) -> Vect n Int -> Nat
f1_vlen Z [] = Z
f1_vlen (S n) ((::) {len = n} x xs) = f1_vlen n xs

You can use a 0-quantified variable (n) on the RHS, as long as it is used only in erased positions. (The variable n is projected out of (::), and the erased argument of f1_vlen is forced to S n.) Since the first argument of f1_vlen is 0-quantified, as you can see in the type signature, it's fine to use erased n in the recursive call in that position.

f1_g : (1 n : Nat) -> Vect n Int -> Nat
f1_g n xs = n `plus` f1_vlen n xs  -- Prelude.plus has a more precise, linear type, unlike method (+)

Here's an a bit contrived example: you use a linearly bound variable (n) twice, but one of the uses is linear and the other is in an erased position, so they add up to 1 and everything is fine.

-- counterexample to "we must use linear arguments on the RHS"
f2_not : (1 _ : Bool) -> Bool
f2_not True = False
f2_not False = True

You don't have to use linearly bound arguments on the RHS if matching consumes them entirely; for example, if they consist only of the constructor tag.

f2_toList : (1 xs : Vect (S n) Bool) -> List Bool
f2_toList ((::) {len = n} x xs) = x :: xs

Here, you match on a linearly bound argument, projecting out field n. Since this field is erased, you need not use it on the RHS, even though its "parent constructor" was bound linearly.

-- counterexample to "we must match on linear arguments"
f2_id : (1 _ : Bool) -> Bool
f2_id x = x

You don't need to match on linear arguments, as long as you ensure that they are consumed. Here, consumption of x is ensured by returning it from the function.

-- not a counterexample, here you both match `S n` *and* use `n` on the RHS
f2_pred : (1 _ : Nat) -> Nat
f2_pred Z = Z
f2_pred (S n) = n

For completeness, as you say, you can also have both matching and a mention on the RHS. The match consumes the constructor tag, and the RHS consumes its only field.

In general, I like to think about the constructor tag as yet another field (consumed by pattern matching), and so the rule is that linearly bound values have to be "consumed exactly once", which means either passing the whole thing into something that "consumes it exactly once", or by breaking it up into components, where each component is "consumed exactly once".

Also, usually, you'd use the word "linearity" for the 1 quantity; the usual word for 0 is "erased" (some people say "irrelevant", but that discussion is yet another can of worms) and \omega is "unrestricted". The general word is "quantity" or "multiplicity".

[donovancrichton]

Cheers @ziman and @andrevidela!

Ok, so there's a lot of intuition I still don't have for linear types then. So I wont chime in too much here and leave it to more experienced heads than mine :).

Do we agree that the current behaviour that moves unrestricted types to erased types through a @-pattern is undesirable?

If not then I think we should carefully document why this happens (along with examples) in the official docs to make it clear to everyone :).

[andrevidela]

Do we agree that the current behaviour that moves unrestricted types to erased types through a @-pattern is undesirable?

at first glance it looks like a bug to me :)

[ziman]

What I find the most confusing here is that it's a, which is not @-bound, that switches to 0.

[donovancrichton]

There might be some issues with shadowing going on with my previous example. Here it is again to be more specific:

data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

f : MyList b -> ()
f [] = ()
f ((::) {a} x xs) = ?normal

g : MyList b -> ()
g [] = ()
g l@((::) {a} x xs) = ?no_linearity

where ?normal gives:

   a : Type
   x : a
   xs : MyList a
 0 b : Type
-------------------------------------
normal : ()

and ?no_linearity gives:

 0 a : Type
   x : a
   xs : MyList a
   l : MyList a
 0 b : Type
-------------------------------------
no_linearity : ()

b is correctly erased in both examples :)