idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Describe what is meant by "use"

Browse Source 
I hit a roadblock trying to understand linear types, because I couldn't figure out what is meant to "use" a variable. I eventually think I figured it out, by reading "Linear types can change the world!", but it was not easy to do so. I think a better description of what "use" means would be very helpful for those unfamiliar with linear types, so I took a stab at it. Hope it helps.
This commit is contained in:
Tim Engler 2020-06-30 19:16:59 +08:00 committed by G. Allais
parent 066b37feb4
commit 14725dac67
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
docs/source/tutorial/multiplicities.rst
View File

@ -72,6 +72,11 @@ Linearity
---------
The ``1`` multiplicity expresses that a variable must be used exactly once.
By "used" we mean either:
* if the variable is a data type or primitive value, it is pattern matched against, ex. by being the subject of a *case* statement, or a function argument that is pattern matched against, etc.,
* if the variable is a function, that function is applied (i.e. ran with an argument)
First, we'll see how this works on some small examples of functions and
data types, then see how it can be used to encode `resource protocols`_.