4Uniqueness Types are an experimental feature available from Idris
50.9.15. A value with a unique type is guaranteed to have *at most one*
6reference to it at run-time, which means that it can safely be updated
7in-place, reducing the need for memory allocation and garbage
8collection. The motivation is that we would like to be able to write
9reactive systems, programs which run in limited memory environments,
10device drivers, and any other system with hard real-time requirements,
11ideally while giving up as little high level conveniences as possible.
13They are inspired by linear types, `Uniqueness Types
14<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean
15<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
16ownership types and borrowed pointers in the `Rust
17<http://www.rust-lang.org/>`__ programming language.
19Some things we hope to be able to do eventually with uniqueness types
22- Safe, pure, in-place update of arrays, lists, etc
23- Provide guarantees of correct resource usage, state transitions, etc
24- Provide guarantees that critical program fragments will *never*
30If ``x : T`` and ``T : UniqueType``, then there is at most one reference
31to ``x`` at any time during run-time execution. For example, we can
32declare the type of unique lists as follows:
36 data UList : Type -> UniqueType
38 (::) : a -> UList a -> UList a
40If we have a value ``xs : UList a``, then there is at most one
41reference to ``xs`` at run-time. The type checker preserves this
42guarantee by ensuring that there is at most one reference to any value
43of a unique type in a pattern clause. For example, the following
44function definition would be valid:
48 umap : (a -> b) -> UList a -> UList b
50 umap f (x :: xs) = f x :: umap f xs
52In the second clause, ``xs`` is a value of a unique type, and only
53appears once on the right hand side, so this clause is valid. Not only
54that, since we know there can be no other reference to the ``UList a``
55argument, we can reuse its space for building the result! The compiler
56is aware of this, and compiles this definition to an in-place update
59The following function definition would not be valid (even assuming an
60implementation of ``++``), however, since ``xs`` appears twice:
64 dupList : UList a -> UList a
67This would result in a shared pointer to ``xs``, so the typechecker
72 unique.idr:12:5:Unique name xs is used more than once
74If we explicitly copy, however, the typechecker is happy:
78 dup : UList a -> UList a
80 dup (x :: xs) = x :: x :: dup xs
82Note that it's fine to use ``x`` twice, because ``a`` is a ``Type``,
83rather than a ``UniqueType``.
85There are some other restrictions on where a ``UniqueType`` can
86appear, so that the uniqueness property is preserved. In particular,
87the type of the function type, ``(x : a) -> b`` depends on the type of
88``a`` or ``b`` - if either is a ``UniqueType``, then the function type
89is also a ``UniqueType``. Then, in a data declaration, if the type
90constructor builds a ``Type``, then no constructor can have a
91``UniqueType``. For example, the following definition is invalid,
92since it would embed a unique value in a possible non-unique value:
96 data BadList : UniqueType -> Type
97 Nil : {a : UniqueType} -> BadList a
98 (::) : {a : UniqueType} -> a -> BadList a -> BadList a
100Finally, types may be polymorphic in their uniqueness, to a limited
101extent. Since ``Type`` and ``UniqueType`` are different types, we are
102limited in how much we can use polymorphic functions on unique types.
103For example, if we have function composition defined as follows:
107 (.) : {a, b, c : Type} -> (b -> c) -> (a -> b) -> a -> c
110And we have some functions over unique types:
114 foo : UList a -> UList b
115 bar : UList b -> UList c
117Then we cannot compose ``foo`` and ``bar`` as ``bar . foo``, because
118``UList`` does not compute a ``Type``! Instead, we can define
119composition as follows:
123 (.) : {a, b, c : Type*} -> (b -> c) -> (a -> b) -> a -> c
126The ``Type*`` type stands for either unique or non-unique types. Since
127such a function may be passed a ``UniqueType``, any value of type
128``Type*`` must also satisfy the requirement that it appears at most
129once on the right hand side.
134It quickly becomes obvious when working with uniqueness types that
135having only one reference at a time can be painful. For example, what
136if we want to display a list before updating it?
140 showU : Show a => UList a -> String
141 showU xs = "[" ++ showU' xs ++ "]" where
142 showU' : UList a -> String
145 showU' (x :: xs) = show x ++ ", " ++ showU' xs
147This is a valid definition of ``showU``, but unfortunately it consumes
148the list! So the following function would be invalid:
152 printAndUpdate : UList Int -> IO ()
153 printAndUpdate xs = do putStrLn (showU xs)
154 let xs' = umap (*2) xs -- xs no longer available!
157Still, one would hope to be able to display a unique list without
158problem, since it merely *inspects* the list; there are no updates. We
159can achieve this, using the notion of *borrowing*. A Borrowed type is
160a Unique type which can be inspected at the top level (by pattern
161matching, or by *lending* to another function) but no further. This
162ensures that the internals (i.e. the arguments to top level patterns)
163will not be passed to any function which will update them.
165``Borrowed`` converts a ``UniqueType`` to a ``BorrowedType``. It is
166defined as follows (along with some additional rules in the
171 data Borrowed : UniqueType -> BorrowedType where
172 Read : {a : UniqueType} -> a -> Borrowed a
175 lend : {a : UniqueType} -> a -> Borrowed a
178A value can be "lent" to another function using ``lend``. Arguments to
179``lend`` are not counted by the type checker as a reference to a unique
180value, therefore a value can be lent as many times as desired. Using
181this, we can write ``showU`` as follows:
185 showU : Show a => Borrowed (UList a) -> String
186 showU xs = "[" ++ showU' xs ++ "]" where
187 showU' : Borrowed (UList a) -> String
190 showU' (Read (x :: xs)) = show x ++ ", " ++ showU' (lend xs)
192Unlike a unique value, a borrowed value may be referred to as many
193times as desired. However, there is a restriction on how a borrowed
194value can be used. After all, much like a library book or your
195neighbour's lawnmower, if a function borrows a value it is expected to
196return it in exactly the condition in which it was received!
198The restriction is that when a ``Borrowed`` type is matched, any
199pattern variables under the ``Read`` which have a unique type may not
200be referred to at all on the right hand side (unless they are
201themselves ``lent`` to another function).
203Uniqueness information is stored in the type, and in particular in
204function types. Once we're in a unique context, any new function which
205is constructed will be required to have unique type, which prevents
206the following sort of bad program being implemented:
210 foo : UList Int -> IO ()
211 foo xs = do let f = \x : Int => showU xs
216Since ``lend`` is implicit, in practice for functions to lend and borrow
217values merely requires the argument to be marked as ``Borrowed``. We can
218therefore write ``showU`` as follows:
222 showU : Show a => Borrowed (UList a) -> String
223 showU xs = "[" ++ showU' xs ++ "]" where
224 showU' : Borrowed (UList a) -> String
227 showU' (x :: xs) = show x ++ ", " ++ showU' xs
229Problems/Disadvantages/Still to do...
230~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
232This is a work in progress, there is lots to do. The most obvious
233problem is the loss of abstraction. On the one hand, we have more
234precise control over memory usage with ``UniqueType`` and
235``BorrowedType``, but they are not in general compatible with
236functions polymorphic over ``Type``. In the short term, we can start
237to write reactive and low memory systems with this, but longer term it
238would be nice to support more abstraction.
240We also haven't checked any of the metatheory, so this could all be
241fatally flawed! The implementation is based to a large extent on
242`Uniqueness Typing Simplified
243<http://lambda-the-ultimate.org/node/2708>`__, by de Vries et al, so
244there is reason to believe things should be fine, but we still have to
247Much as there are with linear types, there are some annoyances when
248trying to prove properties of functions with unique types (for
249example, what counts as a use of a value). Since we require *at most*
250one use of a value, rather than *exactly* one, this seems to be less
251of an issue in practice, but still needs thought.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list