- Author
- The Idris Community
- Published
- Undated; copyright 2020-2023
- Kind
- Official language documentation, a tutorial page with code examples
- Original
- idris2.readthedocs.io/en/latest/tutorial/multiplicities.html
- Subject
- Programming languages and types
What it is
The Idris Community wrote this page for the Idris 2 documentation. It teaches the three quantities a variable can have. It then shows what each one allows in a program.
What it says
- The page says Idris 2 rests on Quantitative Type Theory, giving each variable a quantity.
- A quantity is 0 for erased, 1 for used exactly once, or unrestricted.
- Linear arguments let types encode resource protocols, such as a door opened, closed, then deleted.
- Leaving out the final delete step in the door example fails type checking.
- Idris 2 implements IO with a world token that is always used linearly.
- Implicitly bound names are erased. Matching on an erased argument is rejected unless its value is inferable.
- Types can be matched on, and only multiplicity 0 arguments are truly parametric.
What evidence it gives
The page walks through small code examples. It shows hole types and error messages from the Idris 2 checker. It points to a separate paper for details.
Interests and limits
The authors maintain the language, so the page presents its design favorably. It is a tutorial, not a formal treatment. It lists open questions, such as whether linearity could guide memory management. The page is undated.