git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/docs/reference/uniqueness-types.rst
252 lines 9.5 kB history raw
1****************
2Uniqueness Types
3****************
5Uniqueness Types are an experimental feature available from Idris
60.9.15. A value with a unique type is guaranteed to have *at most one*
7reference to it at run-time, which means that it can safely be updated
8in-place, reducing the need for memory allocation and garbage
9collection. The motivation is that we would like to be able to write
10reactive systems, programs which run in limited memory environments,
11device drivers, and any other system with hard real-time requirements,
12ideally while giving up as little high level conveniences as possible.
14They are inspired by linear types, `Uniqueness Types
15<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean
16<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
17ownership types and borrowed pointers in the `Rust
18<http://www.rust-lang.org/>`__ programming language.
20Some things we hope to be able to do eventually with uniqueness types
21include:
23- Safe, pure, in-place update of arrays, lists, etc
24- Provide guarantees of correct resource usage, state transitions, etc
25- Provide guarantees that critical program fragments will *never*
26 allocate
28Using Uniqueness
29================
31If ``x : T`` and ``T : UniqueType``, then there is at most one reference
32to ``x`` at any time during run-time execution. For example, we can
33declare the type of unique lists as follows:
35.. code-block:: idris
37 data UList : Type -> UniqueType
38 Nil : UList a
39 (::) : a -> UList a -> UList a
41If we have a value ``xs : UList a``, then there is at most one
42reference to ``xs`` at run-time. The type checker preserves this
43guarantee by ensuring that there is at most one reference to any value
44of a unique type in a pattern clause. For example, the following
45function definition would be valid:
47.. code-block:: idris
49 umap : (a -> b) -> UList a -> UList b
50 umap f [] = []
51 umap f (x :: xs) = f x :: umap f xs
53In the second clause, ``xs`` is a value of a unique type, and only
54appears once on the right hand side, so this clause is valid. Not only
55that, since we know there can be no other reference to the ``UList a``
56argument, we can reuse its space for building the result! The compiler
57is aware of this, and compiles this definition to an in-place update
58of the list.
60The following function definition would not be valid (even assuming an
61implementation of ``++``), however, since ``xs`` appears twice:
63.. code-block:: idris
65 dupList : UList a -> UList a
66 dupList xs = xs ++ xs
68This would result in a shared pointer to ``xs``, so the typechecker
69reports:
71.. code-block:: idris
73 unique.idr:12:5:Unique name xs is used more than once
75If we explicitly copy, however, the typechecker is happy:
77.. code-block:: idris
79 dup : UList a -> UList a
80 dup [] = []
81 dup (x :: xs) = x :: x :: dup xs
83Note that it's fine to use ``x`` twice, because ``a`` is a ``Type``,
84rather than a ``UniqueType``.
86There are some other restrictions on where a ``UniqueType`` can
87appear, so that the uniqueness property is preserved. In particular,
88the type of the function type, ``(x : a) -> b`` depends on the type of
89``a`` or ``b`` - if either is a ``UniqueType``, then the function type
90is also a ``UniqueType``. Then, in a data declaration, if the type
91constructor builds a ``Type``, then no constructor can have a
92``UniqueType``. For example, the following definition is invalid,
93since it would embed a unique value in a possible non-unique value:
95.. code-block:: idris
97 data BadList : UniqueType -> Type
98 Nil : {a : UniqueType} -> BadList a
99 (::) : {a : UniqueType} -> a -> BadList a -> BadList a
101Finally, types may be polymorphic in their uniqueness, to a limited
102extent. Since ``Type`` and ``UniqueType`` are different types, we are
103limited in how much we can use polymorphic functions on unique types.
104For example, if we have function composition defined as follows:
106.. code-block:: idris
108 (.) : {a, b, c : Type} -> (b -> c) -> (a -> b) -> a -> c
109 (.) f g x = f (g x)
111And we have some functions over unique types:
113.. code-block:: idris
115 foo : UList a -> UList b
116 bar : UList b -> UList c
118Then we cannot compose ``foo`` and ``bar`` as ``bar . foo``, because
119``UList`` does not compute a ``Type``! Instead, we can define
120composition as follows:
122.. code-block:: idris
124 (.) : {a, b, c : Type*} -> (b -> c) -> (a -> b) -> a -> c
125 (.) f g x = f (g x)
127The ``Type*`` type stands for either unique or non-unique types. Since
128such a function may be passed a ``UniqueType``, any value of type
129``Type*`` must also satisfy the requirement that it appears at most
130once on the right hand side.
132Borrowed Types
133--------------
135It quickly becomes obvious when working with uniqueness types that
136having only one reference at a time can be painful. For example, what
137if we want to display a list before updating it?
139.. code-block:: idris
141 showU : Show a => UList a -> String
142 showU xs = "[" ++ showU' xs ++ "]" where
143 showU' : UList a -> String
144 showU' [] = ""
145 showU' [x] = show x
146 showU' (x :: xs) = show x ++ ", " ++ showU' xs
148This is a valid definition of ``showU``, but unfortunately it consumes
149the list! So the following function would be invalid:
151.. code-block:: idris
153 printAndUpdate : UList Int -> IO ()
154 printAndUpdate xs = do putStrLn (showU xs)
155 let xs' = umap (*2) xs -- xs no longer available!
156 putStrLn (showU xs')
158Still, one would hope to be able to display a unique list without
159problem, since it merely *inspects* the list; there are no updates. We
160can achieve this, using the notion of *borrowing*. A Borrowed type is
161a Unique type which can be inspected at the top level (by pattern
162matching, or by *lending* to another function) but no further. This
163ensures that the internals (i.e. the arguments to top level patterns)
164will not be passed to any function which will update them.
166``Borrowed`` converts a ``UniqueType`` to a ``BorrowedType``. It is
167defined as follows (along with some additional rules in the
168typechecker):
170.. code-block:: idris
172 data Borrowed : UniqueType -> BorrowedType where
173 Read : {a : UniqueType} -> a -> Borrowed a
175 implicit
176 lend : {a : UniqueType} -> a -> Borrowed a
177 lend x = Read x
179A value can be "lent" to another function using ``lend``. Arguments to
180``lend`` are not counted by the type checker as a reference to a unique
181value, therefore a value can be lent as many times as desired. Using
182this, we can write ``showU`` as follows:
184.. code-block:: idris
186 showU : Show a => Borrowed (UList a) -> String
187 showU xs = "[" ++ showU' xs ++ "]" where
188 showU' : Borrowed (UList a) -> String
189 showU' [] = ""
190 showU' [x] = show x
191 showU' (Read (x :: xs)) = show x ++ ", " ++ showU' (lend xs)
193Unlike a unique value, a borrowed value may be referred to as many
194times as desired. However, there is a restriction on how a borrowed
195value can be used. After all, much like a library book or your
196neighbour's lawnmower, if a function borrows a value it is expected to
197return it in exactly the condition in which it was received!
199The restriction is that when a ``Borrowed`` type is matched, any
200pattern variables under the ``Read`` which have a unique type may not
201be referred to at all on the right hand side (unless they are
202themselves ``lent`` to another function).
204Uniqueness information is stored in the type, and in particular in
205function types. Once we're in a unique context, any new function which
206is constructed will be required to have unique type, which prevents
207the following sort of bad program being implemented:
209.. code-block:: idris
211 foo : UList Int -> IO ()
212 foo xs = do let f = \x : Int => showU xs
213 putStrLn $ free xs
214 putStrLn $ f 42
215 return ()
217Since ``lend`` is implicit, in practice for functions to lend and borrow
218values merely requires the argument to be marked as ``Borrowed``. We can
219therefore write ``showU`` as follows:
221.. code-block:: idris
223 showU : Show a => Borrowed (UList a) -> String
224 showU xs = "[" ++ showU' xs ++ "]" where
225 showU' : Borrowed (UList a) -> String
226 showU' [] = ""
227 showU' [x] = show x
228 showU' (x :: xs) = show x ++ ", " ++ showU' xs
230Problems/Disadvantages/Still to do...
231-------------------------------------
233This is a work in progress, there is lots to do. The most obvious
234problem is the loss of abstraction. On the one hand, we have more
235precise control over memory usage with ``UniqueType`` and
236``BorrowedType``, but they are not in general compatible with
237functions polymorphic over ``Type``. In the short term, we can start
238to write reactive and low memory systems with this, but longer term it
239would be nice to support more abstraction.
241We also haven't checked any of the metatheory, so this could all be
242fatally flawed! The implementation is based to a large extent on
243`Uniqueness Typing Simplified
244<http://lambda-the-ultimate.org/node/2708>`__, by de Vries et al, so
245there is reason to believe things should be fine, but we still have to
246do the work.
248Much as there are with linear types, there are some annoyances when
249trying to prove properties of functions with unique types (for
250example, what counts as a use of a value). Since we require *at most*
251one use of a value, rather than *exactly* one, this seems to be less
252of an issue in practice, but still needs thought.