What does the 0 or 1 before a parameter name mean in Idris?

Question

I've seen it here and there in Idris source code, but I have yet to find an explanation for what it means. The closest I've gotten is finding that it's called RigCount in the syntax reference. But what is it?

test : (0 a : b) -> b
test x = x
--      ^^^ Error

As it happens the above example throws an error: While processing right hand side of test. x is not accessible in this context.

Changing this to a 1 makes it type check, but it doesn't give any more indication what it means.

test : (1 a : b) -> b
test x = x

Answer 1

To elaborate on the error message, in the first example, (0 a : b) says there are 0 of a (or x) available at runtime. You'd need it to be available at runtime to return it. Hence, it "is not accessible in this context".

You can make it available in this context in two ways:

• change its multiplicity, which is what you do when you write (1 a : b), which says there are exactly one of these available at runtime. You could also leave off the multiplicity, as (a : b), which means any number are available at runtime, or
• change the context. You can also give module-level objects multiplicities, so if you marked test as erased, like

  0 test : (0 a : b) -> b
  

  then you can return x because you're stating the result of test is also erased.

Answer 2

This is a multiplicity.

Idris2 has three multiplicities:

• Erased (0) - not available at runtime
• Linear (1) - can be used once at runtime
• Unrestricted (no multiplicity tag) - can be used any number of times