1Erasure By Usage Analysis
2=========================
4This work stems from this `feature proposal
5<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__
6(obsoleted by this page). Beware that the information in the proposal
7is out of date — and sometimes even in direct contradiction with the
8eventual implementation.
13Traditional dependently typed languages (Agda, Coq) are good at
14erasing *proofs* (either via irrelevance or an extra universe).
18 half : (n : Nat) -> Even n -> Nat
20 half (S (S n)) (ES pf) = S (half n pf)
22For example, in the above snippet, the second argument is a proof,
23which is used only to convince the compiler that the function is
24total. This proof is never inspected at runtime and thus can be
25erased. In this case, the mere existence of the proof is sufficient
26and we can use irrelevance-related methods to achieve erasure.
28However, sometimes we want to erase *indices* and this is where the
29traditional approaches stop being useful, mainly for reasons described
30in the `original proposal
31<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations#prop-is-cumbersome-coq>`__.
35 uninterleave : {n : Nat} -> Vect (n * 2) a -> (Vect n a, Vect n a)
36 uninterleave [] = ([] , [])
37 uninterleave (x :: y :: rest) with (unzipPairs rest)
38 | (xs, ys) = (x :: xs, y :: ys)
40Notice that in this case, the second argument is the important one and
41we would like to get rid of the ``n`` instead, although the shape of
42the program is generally the same as in the previous case.
44There are methods described by Brady, McBride and McKinna in [BMM04]_
45to remove the indices from data structures, exploiting the fact that
46functions operating on them either already have a copy of the
47appropriate index or the index can be quickly reconstructed if needed.
48However, we often want to erase the indices altogether, from the whole
49program, even in those cases where reconstruction is not possible.
51The following two sections describe two cases where doing so improves
52the runtime performance asymptotically.
57- O(n) instead of O(log n)
59Consider the following ``Nat``-indexed type family representing binary
64 data Bin : Nat -> Type where
66 O : {n : Nat} -> Bin n -> Bin (0 + 2*n)
67 I : {n : Nat} -> Bin n -> Bin (1 + 2*n)
69These are supposed to be (at least asymptotically) fast and
70memory-efficient because their size is logarithmic compared to the
71numbers they represent.
73Unfortunately this is not the case. The problem is that these binary
74numbers still carry the *unary* indices with them, performing
75arithmetic on the indices whenever arithmetic is done on the binary
76numbers themselves. Hence the real representation of the number 15
91The used memory is actually *linear*, not logarithmic and therefore we
92cannot get below O(n) with time complexities.
94One could argue that Idris in fact compiles ``Nat`` via GMP but
95that's a moot point for two reasons:
97+ First, whenever we try to index our datastructures with anything
98 else than ``Nat``, the compiler is not going to come to the rescue.
100+ Second, even with ``Nat``, the GMP integers are *still* there and
101 they slow the runtime down.
103This ought not to be the case since the ``Nat`` are never used at
104runtime and they are only there for typechecking purposes. Hence we
105should get rid of them and get runtime code similar to what a idris
106programmer would write.
111- O(n^2) instead of O(n)
113Consider the type of U-views of lists:
117 data U : List a -> Type where
119 one : (z : a) -> U [z]
120 two : {xs : List a} -> (x : a) -> (u : U xs) -> (y : a) -> U (x :: xs ++ [y])
122For better intuition, the shape of the U-view of
123``[x0,x1,x2,z,y2,y1,y0]`` looks like this:
132When recursing over this structure, the values of ``xs`` range over
133``[x0,x1,x2,z,y2,y1,y0]``, ``[x1,x2,z,y2,y1]``, ``[x2,z,y2]``,
134``[z]``. No matter whether these lists are stored or built on demand,
135they take up a quadratic amount of memory (because they cannot share
136nodes), and hence it takes a quadratic amount of time just to build
137values of this index alone.
139But the reasonable expectation is that operations with U-views take
140linear time — so we need to erase the index ``xs`` if we want to
146Usage analysis is run at every compilation and its outputs are used
147for various purposes. This is actually invisible to the user but it's
148a relatively big and important change, which enables the new features.
150Everything that is found to be unused is erased. No annotations are
151needed, just don't use the thing and it will vanish from the generated
152code. However, if you wish, you can use the dot annotations to get a
153warning if the thing is accidentally used.
155"Being used" in this context means that the value of the "thing" may
156influence run-time behaviour of the program. (More precisely, it is
157not found to be irrelevant to the run-time behaviour by the usage
160"Things" considered for removal by erasure include:
164* data constructor fields (including record fields and dictionary
165 fields of class instances)
167For example, ``Either`` often compiles to the same runtime
168representation as ``Bool``. Constructor field removal sometimes
169combines with the newtype optimisation to have quite a strong effect.
171There is a new compiler option ``--warnreach``, which will enable
172warnings coming from erasure. Since we have full usage analysis, we
173can compile even those programs that violate erasure annotations --
174it's just that the binaries may run slower than expected. The warnings
175will be enabled by default in future versions of Idris (and possibly
176turned to errors). However, in this transitional period, we chose to
177keep them on-demand to avoid confusion until better documentation is
180Case-tree elaboration tries to avoid using dotted "things" whenever
181possible. (NB. This is not yet perfect and it's being worked on:
182https://gist.github.com/ziman/10458331)
184Postulates are no longer required to be collapsible. They are now
185required to be *unused* instead.
187Changes to the language
188-----------------------
190You can use dots to mark fields that are not intended to be used at
195 data Bin : Nat -> Type where
197 O : .{n : Nat} -> Bin n -> Bin (0 + 2*n)
198 I : .{n : Nat} -> Bin n -> Bin (1 + 2*n)
200If these fields are found to be used at runtime, the dots will trigger
201a warning (with ``--warnreach``).
203Note that free (unbound) implicits are dotted by default so, for
204example, the constructor ``O`` can be defined as:
208 O : Bin n -> Bin (0 + 2*n)
210and this is actually the preferred form.
212If you have a free implicit which is meant to be used at runtime, you
213have to change it into an (undotted) ``{bound : implicit}``.
215You can also put dots in types of functions to get more guarantees.
219 half : (n : Nat) -> .(pf : Even n) -> Nat
221and free implicits are automatically dotted here, too.
226Dot annotations serve two purposes:
228* influence case-tree elaboration to avoid dotted variables
230* trigger warnings when a dotted variable is used
232However, there's no direct connection between being dotted and being
233erased. The compiler erases everything it can, dotted or not. The dots
234are there mainly to help the programmer (and the compiler) refrain
235from using the values they want to erase.
240Ideally, few or no extra annotations are needed -- in practice, it
241turns out that having free implicits automatically dotted is enough to
244Therefore, just compile with ``--warnreach`` to see warnings if
245erasure cannot remove parts of the program.
247However, those programs that have been written without runtime
248behaviour in mind, will need some help to get in the form that
249compiles to a reasonable binary. Generally, it's sufficient to follow
250erasure warnings (which may be sometimes unhelpful at the moment).
255- source: https://github.com/ziman/idris-benchmarks
256- results: http://ziman.functor.sk/erasure-bm/
258It can be clearly seen that asymptotics are improved by erasure.
263You can't get warnings in libraries because usage analysis starts from
264``Main.main``. This will be solved by the planned ``%default_usage``
267Usage warnings are quite bad and unhelpful at the moment. We should
268include more information and at least translate argument numbers to
271There is no decent documentation yet. This wiki page is the first one.
273There is no generally accepted terminology. We switch between
274"dotted", "unused", "erased", "irrelevant", "inaccessible", while each
275has a slightly different meaning. We need more consistent and
276understandable naming.
278If the same type is used in both erased and non-erased context, it
279will retain its fields to accomodate the least common denominator --
280the non-erased context. This is particularly troublesome in the case
281of the type of (dependent) pairs, where it actually means that no
282erasure would be performed. We should probably locate disjoint uses of
283data types and split them into "sub-types". There are three different
284flavours of dependent types now: ``Sigma`` (nothing erased),
285``Exists`` (first component erased), ``Subset`` (second component
288Case-tree building does not avoid dotted values coming from
289pattern-matched constructors (https://gist.github.com/ziman/10458331).
290This is to be fixed soon. (Fixed.)
292Higher-order function arguments and opaque functional variables are
293considered to be using all their arguments. To work around this, you
294can force erasure via the type system, using the ``Erased`` wrapper:
295https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr
297Typeclass methods are considered to be using the union of all their
298implementations. In other words, an argument of a method is unused
299only if it is unused in every implementation of the method that occurs
305- Fixes to the above shortcomings in general.
307- Improvements to the case-tree elaborator so that it properly avoids
308 dotted fields of data constructors. Done.
310- Compiler pragma ``%default_usage used/unused`` and per-function
311 overrides ``used`` and ``unused``, which allow the programmer to
312 mark the return value of a function as used, even if the function
313 is not used in ``main`` (which is the case when writing library
314 code). These annotations will help library writers discover usage
315 violations in their code before it is actually published and used
316 in compiled programs.
324The patch introducing erasure by usage analysis also disabled some
325optimisations that were in place before; these are subsumed by the new
326erasure. However, in some erasure-unaware programs, where erasure by
327usage analysis does not exercise its full potential (but the old
328optimisations would have worked), certain slowdown may be observed (up
329to ~10% according to preliminary benchmarking), due to retention and
330computation of information that should not be necessary at runtime.
332A simple check whether this is the case is to compile with
333``--warnreach``. If you see warnings, there is some unnecessary code
334getting compiled into the binary.
336The solution is to change the code so that there are no warnings.
338Usage warnings are unhelpful
339~~~~~~~~~~~~~~~~~~~~~~~~~~~~
341This is a known issue and we are working on it. For now, see the section
342`How to read and resolve erasure
343warnings <#how-to-read-and-resolve-erasure-warnings>`__.
345There should be no warnings in this function
346~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
348A possible cause is non-totality of the function (more precisely,
349non-coverage). If a function is non-covering, the program needs to
350inspect all arguments in order to detect coverage failures at runtime.
351Since the function inspects all its arguments, nothing can be erased
352and this may transitively cause usage violations. The solution is to
353make the function total or accept the fact that it will use its
354arguments and remove some dots from the appropriate constructor fields
355and function arguments. (Please note that this is not a shortcoming of
356erasure and there is nothing we can do about it.)
358Another possible cause is the currently imperfect case-tree
359elaboration, which does not avoid dotted constructor fields (see
360https://gist.github.com/ziman/10458331). You can either rephrase the
361function or wait until this is fixed, hopefully soon. Fixed.
363The compiler refuses to recognise this thing as erased
364~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
366You can force anything to be erased by wrapping it in the ``Erased``
367monad. While this program triggers usage warnings,
371 f : (g : Nat -> Nat) -> .(x : Nat) -> Nat
372 f g x = g x -- WARNING: g uses x
374the following program does not:
378 f : (g : Erased Nat -> Nat) -> .(x : Nat) -> Nat
379 f g x = g (Erase x) -- OK
381How to read and resolve erasure warnings
382----------------------------------------
387Consider the following program:
391 vlen : Vect n a -> Nat
394 sumLengths : List (Vect n a) -> Nat
396 sumLengths (v :: vs) = vlen v + sumLengths vs
399 main = print . sumLengths $ [[0,1],[2,3]]
401When you compile it using ``--warnreach``, there is one warning:
405 Main.sumLengths: inaccessible arguments reachable:
406 n (no more information available)
408The warning does not contain much detail at this point so we can try
409compiling with ``--dumpcases cases.txt`` and look up the compiled
410definition in ``cases.txt``:
414 Main.sumLengths {e0} {e1} {e2} =
416 | Prelude.List.::({e6}) => LPlus (ATInt ITBig)({e0}, Main.sumLengths({e0}, ____, {e6}))
417 | Prelude.List.Nil() => 0
419The reason for the warning is that ``sumLengths`` calls ``vlen``, which
420gets inlined. The second clause of ``sumLengths`` then accesses the
421variable ``n``, compiled as ``{e0}``. Since ``n`` is a free implicit, it
422is automatically considered dotted and this triggers the warning.
424A solution would be either making the argument ``n`` a bound implicit
425parameter to indicate that we wish to keep it at runtime,
429 sumLengths : {n : Nat} -> List (Vect n a) -> Nat
431or fixing ``vlen`` to not use the index:
435 vlen : Vect n a -> Nat
437 vlen (x :: xs) = S (vlen xs)
439Which solution is appropriate depends on the usecase.
444Consider the following program manipulating value-indexed binary
449 data Bin : Nat -> Type where
451 O : Bin n -> Bin (0 + n + n)
452 I : Bin n -> Bin (1 + n + n)
454 toN : (b : Bin n) -> Nat
456 toN (O {n} bs) = 0 + n + n
457 toN (I {n} bs) = 1 + n + n
460 main = print . toN $ I (I (O (O (I N))))
462In the function ``toN``, we attempted to "cheat" and instead of
463traversing the whole structure, we just projected the value index ``n``
464out of constructors ``I`` and ``O``. However, this index is a free
465implicit, therefore it is considered dotted.
467Inspecting it then produces the following warnings when compiling with
472 Main.I: inaccessible arguments reachable:
473 n from Main.toN arg# 1
474 Main.O: inaccessible arguments reachable:
475 n from Main.toN arg# 1
477We can see that the argument ``n`` of both ``I`` and ``O`` is used in
478the function ``toN``, argument 1.
480At this stage of development, warnings only contain argument numbers,
481not names; this will hopefully be fixed. When numbering arguments, we
482go from 0, taking free implicits first, left-to-right; then the bound
483arguments. The function ``toN`` has therefore in fact two arguments:
484``n`` (argument 0) and ``b`` (argument 1). And indeed, as the warning
485says, we project the dotted field from ``b``.
487Again, one solution is to fix the function ``toN`` to calculate its
488result honestly; the other one is to accept that we carry a ``Nat``
489with every constructor of ``Bin`` and make it a bound implicit:
493 O : {n : Nat} -> Bin n -> Bin (0 + n + n)
494 I : {n : Nat} -> bin n -> Bin (1 + n + n)
499.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive
500 families need not store their indices
501 <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