Note nº1: Emulating exact usage in Idris2

Idris2 is a programming language featuring Quantitative Type Theory. In its current implementation Idris2 uses the semiring \(\{0, 1, \omega\}\) which represent usage of a variable. Here, 0 indicates erasure 1 indicates linearity and ω represents unrestricted usage.

Here is an example:

map : (f : (1 v : a) -> b) -> (1 ls : LList a) -> LList b
map f [] = []
map f (x :: xs) = f x :: map f xs

This is the map function defined on linear lists, a linear list is just like a list, except all its constructors are linear, which means we must consume each list exactly once.

As you can see, the function f is also linear, it takes a v : a that can be used only once and return a value of type b. Crucially, you will notice that f itself does not have a quantity associated with it, that means it's unrestricted, it can be used however meany times we want (including 0 times).

Now let's do the same with vectors:

map : (f : (1 v : a) -> b) -> (1 vs : LVect n a) -> LVect n b
map f [] = []
map f (x :: xs) = f x :: map f xs

In terms of implementation, this is what we expected. But notice the type signature: It is unchanged, even if we know how many times f will be used. It will be used exactly n times.

This is because Idris2's semiring does not allow us to express exact usage beyond 0 and 1 use. However we can trick it:

map : (0 f : (1 v : a) -> b) -> {auto 1 copies : Copies n f} -> (1 vs : LVect n a) -> LVect n b
map f [] {copies = Done} = []
map f (x :: xs) {copies = (More f cs)} = f x :: map f xs {copies=cs}

In this program f has 0 uses, however it is accompanied with copies which holds n copies of f itself. Since copies has usage 1 it must be entirely consumed, forcing us to make use of every since copy that's available to us. In the implementation we pattern-match on copiesin order to extract the relevant (pun intended) copy of f and use it on the values of the vectors to create a new vector. The auto keyword is just there so that we don't have to write down the copies manually every time we want to use map.

The only mystery remaining is to explain how Copies is implemented. And it's fortunately fairly simple: It's a linear vector that can only keep one single element.

data Copies : Nat -> (0 v : a) -> Type where
  Done : Copies 0 v
  More : (1 v : a) -> (1 _ : Copies n v) -> Copies (S n) v

This way if we have a value Copies 3 "hello" we get three copies of the value "hello". You will notice in the type of Copies that the value itself must have 0 uses, that's because this only occurs in the type the value must be sorted in the More constructor rather than be pulled from the type.

Just to check it works we can write a simple test:

testMap : Vectors.map LSucc [0,1,2,3] === [1,2,3,4]
testMap = Refl

Where LSucc is the successor function for linear Nat.

Thanks to Copies we can now write programs that indicate exactly how many times a variable is used, even if the usage values we have are only 0 1 and ω.