1*************************
2Erasure By Usage Analysis
3*************************
5This work stems from this `feature proposal
6<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__
7(obsoleted by this page). Beware that the information in the proposal
8is out of date — and sometimes even in direct contradiction with the
9eventual implementation.
14Traditional dependently typed languages (Agda, Coq) are good at
15erasing *proofs* (either via irrelevance or an extra universe).
19 half : (n : Nat) -> Even n -> Nat
21 half (S (S n)) (ES pf) = S (half n pf)
23For example, in the above snippet, the second argument is a proof,
24which is used only to convince the compiler that the function is
25total. This proof is never inspected at runtime and thus can be
26erased. In this case, the mere existence of the proof is sufficient
27and we can use irrelevance-related methods to achieve erasure.
29However, sometimes we want to erase *indices* and this is where the
30traditional approaches stop being useful, mainly for reasons described
31in the `original proposal
32<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.
36 uninterleave : {n : Nat} -> Vect (n * 2) a -> (Vect n a, Vect n a)
37 uninterleave [] = ([] , [])
38 uninterleave (x :: y :: rest) with (unzipPairs rest)
39 | (xs, ys) = (x :: xs, y :: ys)
41Notice that in this case, the second argument is the important one and
42we would like to get rid of the ``n`` instead, although the shape of
43the program is generally the same as in the previous case.
45There are methods described by Brady, McBride and McKinna in [BMM04]_
46to remove the indices from data structures, exploiting the fact that
47functions operating on them either already have a copy of the
48appropriate index or the index can be quickly reconstructed if needed.
49However, we often want to erase the indices altogether, from the whole
50program, even in those cases where reconstruction is not possible.
52The following two sections describe two cases where doing so improves
53the runtime performance asymptotically.
58- O(n) instead of O(log n)
60Consider the following ``Nat``-indexed type family representing binary
65 data Bin : Nat -> Type where
67 O : {n : Nat} -> Bin n -> Bin (0 + 2*n)
68 I : {n : Nat} -> Bin n -> Bin (1 + 2*n)
70These are supposed to be (at least asymptotically) fast and
71memory-efficient because their size is logarithmic compared to the
72numbers they represent.
74Unfortunately this is not the case. The problem is that these binary
75numbers still carry the *unary* indices with them, performing
76arithmetic on the indices whenever arithmetic is done on the binary
77numbers themselves. Hence the real representation of the number 15
92The used memory is actually *linear*, not logarithmic and therefore we
93cannot get below O(n) with time complexities.
95One could argue that Idris in fact compiles ``Nat`` via GMP but
96that's a moot point for two reasons:
98+ First, whenever we try to index our datastructures with anything
99 else than ``Nat``, the compiler is not going to come to the rescue.
101+ Second, even with ``Nat``, the GMP integers are *still* there and
102 they slow the runtime down.
104This ought not to be the case since the ``Nat`` are never used at
105runtime and they are only there for typechecking purposes. Hence we
106should get rid of them and get runtime code similar to what a idris
107programmer would write.
112- O(n^2) instead of O(n)
114Consider the type of U-views of lists:
118 data U : List a -> Type where
120 one : (z : a) -> U [z]
121 two : {xs : List a} -> (x : a) -> (u : U xs) -> (y : a) -> U (x :: xs ++ [y])
123For better intuition, the shape of the U-view of
124``[x0,x1,x2,z,y2,y1,y0]`` looks like this:
133When recursing over this structure, the values of ``xs`` range over
134``[x0,x1,x2,z,y2,y1,y0]``, ``[x1,x2,z,y2,y1]``, ``[x2,z,y2]``,
135``[z]``. No matter whether these lists are stored or built on demand,
136they take up a quadratic amount of memory (because they cannot share
137nodes), and hence it takes a quadratic amount of time just to build
138values of this index alone.
140But the reasonable expectation is that operations with U-views take
141linear time — so we need to erase the index ``xs`` if we want to
147Usage analysis is run at every compilation and its outputs are used
148for various purposes. This is actually invisible to the user but it's
149a relatively big and important change, which enables the new features.
151Everything that is found to be unused is erased. No annotations are
152needed, just don't use the thing and it will vanish from the generated
153code. However, if you wish, you can use the dot annotations to get a
154warning if the thing is accidentally used.
156"Being used" in this context means that the value of the "thing" may
157influence run-time behaviour of the program. (More precisely, it is
158not found to be irrelevant to the run-time behaviour by the usage
161"Things" considered for removal by erasure include:
165* data constructor fields (including record fields and dictionary
166 fields of class instances)
168For example, ``Either`` often compiles to the same runtime
169representation as ``Bool``. Constructor field removal sometimes
170combines with the newtype optimisation to have quite a strong effect.
172There is a new compiler option ``--warnreach``, which will enable
173warnings coming from erasure. Since we have full usage analysis, we
174can compile even those programs that violate erasure annotations --
175it's just that the binaries may run slower than expected. The warnings
176will be enabled by default in future versions of Idris (and possibly
177turned to errors). However, in this transitional period, we chose to
178keep them on-demand to avoid confusion until better documentation is
181Case-tree elaboration tries to avoid using dotted "things" whenever
182possible. (NB. This is not yet perfect and it's being worked on:
183https://gist.github.com/ziman/10458331)
185Postulates are no longer required to be collapsible. They are now
186required to be *unused* instead.
188Changes to the language
189=======================
191You can use dots to mark fields that are not intended to be used at
196 data Bin : Nat -> Type where
198 O : .{n : Nat} -> Bin n -> Bin (0 + 2*n)
199 I : .{n : Nat} -> Bin n -> Bin (1 + 2*n)
201If these fields are found to be used at runtime, the dots will trigger
202a warning (with ``--warnreach``).
204Note that free (unbound) implicits are dotted by default so, for
205example, the constructor ``O`` can be defined as:
209 O : Bin n -> Bin (0 + 2*n)
211and this is actually the preferred form.
213If you have a free implicit which is meant to be used at runtime, you
214have to change it into an (undotted) ``{bound : implicit}``.
216You can also put dots in types of functions to get more guarantees.
220 half : (n : Nat) -> .(pf : Even n) -> Nat
222and free implicits are automatically dotted here, too.
227Dot annotations serve two purposes:
229* influence case-tree elaboration to avoid dotted variables
231* trigger warnings when a dotted variable is used
233However, there's no direct connection between being dotted and being
234erased. The compiler erases everything it can, dotted or not. The dots
235are there mainly to help the programmer (and the compiler) refrain
236from using the values they want to erase.
241Ideally, few or no extra annotations are needed -- in practice, it
242turns out that having free implicits automatically dotted is enough to
245Therefore, just compile with ``--warnreach`` to see warnings if
246erasure cannot remove parts of the program.
248However, those programs that have been written without runtime
249behaviour in mind, will need some help to get in the form that
250compiles to a reasonable binary. Generally, it's sufficient to follow
251erasure warnings (which may be sometimes unhelpful at the moment).
256- source: https://github.com/ziman/idris-benchmarks
257- results: http://ziman.functor.sk/erasure-bm/
259It can be clearly seen that asymptotics are improved by erasure.
264You can't get warnings in libraries because usage analysis starts from
265``Main.main``. This will be solved by the planned ``%default_usage``
268Usage warnings are quite bad and unhelpful at the moment. We should
269include more information and at least translate argument numbers to
272There is no decent documentation yet. This wiki page is the first one.
274There is no generally accepted terminology. We switch between
275"dotted", "unused", "erased", "irrelevant", "inaccessible", while each
276has a slightly different meaning. We need more consistent and
277understandable naming.
279If the same type is used in both erased and non-erased context, it
280will retain its fields to accomodate the least common denominator --
281the non-erased context. This is particularly troublesome in the case
282of the type of (dependent) pairs, where it actually means that no
283erasure would be performed. We should probably locate disjoint uses of
284data types and split them into "sub-types". There are three different
285flavours of dependent types now: ``Sigma`` (nothing erased),
286``Exists`` (first component erased), ``Subset`` (second component
289Case-tree building does not avoid dotted values coming from
290pattern-matched constructors (https://gist.github.com/ziman/10458331).
291This is to be fixed soon. (Fixed.)
293Higher-order function arguments and opaque functional variables are
294considered to be using all their arguments. To work around this, you
295can force erasure via the type system, using the ``Erased`` wrapper:
296https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr
298Typeclass methods are considered to be using the union of all their
299implementations. In other words, an argument of a method is unused
300only if it is unused in every implementation of the method that occurs
306- Fixes to the above shortcomings in general.
308- Improvements to the case-tree elaborator so that it properly avoids
309 dotted fields of data constructors. Done.
311- Compiler pragma ``%default_usage used/unused`` and per-function
312 overrides ``used`` and ``unused``, which allow the programmer to
313 mark the return value of a function as used, even if the function
314 is not used in ``main`` (which is the case when writing library
315 code). These annotations will help library writers discover usage
316 violations in their code before it is actually published and used
317 in compiled programs.
325The patch introducing erasure by usage analysis also disabled some
326optimisations that were in place before; these are subsumed by the new
327erasure. However, in some erasure-unaware programs, where erasure by
328usage analysis does not exercise its full potential (but the old
329optimisations would have worked), certain slowdown may be observed (up
330to ~10% according to preliminary benchmarking), due to retention and
331computation of information that should not be necessary at runtime.
333A simple check whether this is the case is to compile with
334``--warnreach``. If you see warnings, there is some unnecessary code
335getting compiled into the binary.
337The solution is to change the code so that there are no warnings.
339Usage warnings are unhelpful
340----------------------------
342This is a known issue and we are working on it. For now, see the section
343`How to read and resolve erasure
344warnings <#how-to-read-and-resolve-erasure-warnings>`__.
346There should be no warnings in this function
347--------------------------------------------
349A possible cause is non-totality of the function (more precisely,
350non-coverage). If a function is non-covering, the program needs to
351inspect all arguments in order to detect coverage failures at runtime.
352Since the function inspects all its arguments, nothing can be erased
353and this may transitively cause usage violations. The solution is to
354make the function total or accept the fact that it will use its
355arguments and remove some dots from the appropriate constructor fields
356and function arguments. (Please note that this is not a shortcoming of
357erasure and there is nothing we can do about it.)
359Another possible cause is the currently imperfect case-tree
360elaboration, which does not avoid dotted constructor fields (see
361https://gist.github.com/ziman/10458331). You can either rephrase the
362function or wait until this is fixed, hopefully soon. Fixed.
364The compiler refuses to recognise this thing as erased
365------------------------------------------------------
367You can force anything to be erased by wrapping it in the ``Erased``
368monad. While this program triggers usage warnings,
372 f : (g : Nat -> Nat) -> .(x : Nat) -> Nat
373 f g x = g x -- WARNING: g uses x
375the following program does not:
379 f : (g : Erased Nat -> Nat) -> .(x : Nat) -> Nat
380 f g x = g (Erase x) -- OK
382How to read and resolve erasure warnings
383========================================
388Consider the following program:
392 vlen : Vect n a -> Nat
395 sumLengths : List (Vect n a) -> Nat
397 sumLengths (v :: vs) = vlen v + sumLengths vs
400 main = print . sumLengths $ [[0,1],[2,3]]
402When you compile it using ``--warnreach``, there is one warning:
406 Main.sumLengths: inaccessible arguments reachable:
407 n (no more information available)
409The warning does not contain much detail at this point so we can try
410compiling with ``--dumpcases cases.txt`` and look up the compiled
411definition in ``cases.txt``:
415 Main.sumLengths {e0} {e1} {e2} =
417 | Prelude.List.::({e6}) => LPlus (ATInt ITBig)({e0}, Main.sumLengths({e0}, ____, {e6}))
418 | Prelude.List.Nil() => 0
420The reason for the warning is that ``sumLengths`` calls ``vlen``, which
421gets inlined. The second clause of ``sumLengths`` then accesses the
422variable ``n``, compiled as ``{e0}``. Since ``n`` is a free implicit, it
423is automatically considered dotted and this triggers the warning.
425A solution would be either making the argument ``n`` a bound implicit
426parameter to indicate that we wish to keep it at runtime,
430 sumLengths : {n : Nat} -> List (Vect n a) -> Nat
432or fixing ``vlen`` to not use the index:
436 vlen : Vect n a -> Nat
438 vlen (x :: xs) = S (vlen xs)
440Which solution is appropriate depends on the usecase.
445Consider the following program manipulating value-indexed binary
450 data Bin : Nat -> Type where
452 O : Bin n -> Bin (0 + n + n)
453 I : Bin n -> Bin (1 + n + n)
455 toN : (b : Bin n) -> Nat
457 toN (O {n} bs) = 0 + n + n
458 toN (I {n} bs) = 1 + n + n
461 main = print . toN $ I (I (O (O (I N))))
463In the function ``toN``, we attempted to "cheat" and instead of
464traversing the whole structure, we just projected the value index ``n``
465out of constructors ``I`` and ``O``. However, this index is a free
466implicit, therefore it is considered dotted.
468Inspecting it then produces the following warnings when compiling with
473 Main.I: inaccessible arguments reachable:
474 n from Main.toN arg# 1
475 Main.O: inaccessible arguments reachable:
476 n from Main.toN arg# 1
478We can see that the argument ``n`` of both ``I`` and ``O`` is used in
479the function ``toN``, argument 1.
481At this stage of development, warnings only contain argument numbers,
482not names; this will hopefully be fixed. When numbering arguments, we
483go from 0, taking free implicits first, left-to-right; then the bound
484arguments. The function ``toN`` has therefore in fact two arguments:
485``n`` (argument 0) and ``b`` (argument 1). And indeed, as the warning
486says, we project the dotted field from ``b``.
488Again, one solution is to fix the function ``toN`` to calculate its
489result honestly; the other one is to accept that we carry a ``Nat``
490with every constructor of ``Bin`` and make it a bound implicit:
494 O : {n : Nat} -> Bin n -> Bin (0 + n + n)
495 I : {n : Nat} -> bin n -> Bin (1 + n + n)
500.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive
501 families need not store their indices
502 <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__
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