1****************************************
2Static Arguments and Partial Evaluation
3****************************************
5As of version 0.9.15, Idris has support for *partial evaluation* of
6statically known arguments. This involves creating specialised versions
7of functions with arguments annotated as ``%static``.
9(This is an implementation of the partial evaluator described in `this
11paper <https://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
12Please refer to this for more precise definitions of what follows.)
14Partial evaluation is switched off by default since Idris 1.0. It can
15be enabled with the ``--partial-eval`` flag.
20Consider the power function over natural numbers, defined as follows
21(we'll call it ``my_pow`` since ``pow`` already exists in the Prelude):
25 my_pow : Nat -> Nat -> Nat
27 my_pow x (S k) = mult x (my_pow x k)
29This is implemented by recursion on the second argument, and we can
30evaluate the definition further if the second argument is known, even if
31the first isn't. For example, we can build a function at the REPL to
32cube a number as follows:
36 *pow> \x => my_pow x 3
37 \x => mult x (mult x (mult x 1)) : Nat -> Nat
41Note that in the resulting function the recursion has been eliminated,
42since ``my_pow`` is implemented by recursion on the known argument. We
43have no such luck if the first argument is known and the second isn't:
47 *pow> \x => my_pow 2 x
48 \x => my_pow 2 x : Nat -> Nat
50Now, consider the following definition which calculates x^2 + 1:
55 powFn x = plus (my_pow x (S (S Z))) (S Z)
57Since the second argument to ``my_pow`` here is statically known, it
58seems a shame to have to make the recursive calls every time. However,
59Idris will not in general inline recursive definitions, in particular
60since they may diverge or duplicate work without some deeper analysis.
62We can, however, give Idris some hints that here we really would like to
63create a specialised version of ``my_pow``.
65Automatic specialisation of ``pow``
66~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68The trick is to mark the statically known arguments with the
73 my_pow : Nat -> %static Nat -> Nat
75 my_pow k (S j) = mult k (my_pow k j)
77When an argument is annotated in this way, Idris will try to create a
78specialised version whenever it accounts a call with a concrete value
79(i.e. a constant, constructor form, or globally defined function) in a
80``%static`` position. If ``my_pow`` is defined this way, and ``powFn``
81defined as above, we can see the effect by typing ``:printdef powFn`` at
88 powFn x = plus (PE_my_pow_3f3e5ad8 x) 1
90What is this mysterious ``PE_my_pow_3f3e5ad8``? It's a specialised power
91function where the statically known argument has been specialised away.
92The name is generated from a hash of the specialised arguments, and we
93can see its definition with ``:printdef`` too:
97 *petest> :printdef PE_my_pow_3f3e5ad8
98 PE_my_pow_3f3e5ad8 : Nat -> Nat
99 PE_my_pow_3f3e5ad8 (0arg) = mult (0arg) (mult (0arg) (PE_fromInteger_7ba9767f 1))
101The ``(0arg)`` is an internal argument name (programmers can't give
102variable names beginning with a digit after all). Notice also that there
103is a specialised version of ``fromInteger`` for ``Nat``\ s, since type
104class dictionaries are themselves a particularly common case of
105statically known arguments!
107Specialising Type Classes
108-------------------------
110Type class dictionaries are very often statically known, so Idris
111automatically marks any type class constraint as ``%static`` and builds
112specialised versions of top level functions where the class is
113instantiated. For example, given:
120If we print this definition, we'll see a specialised version of ``+`` is
125 *petest> :printdef calc
127 calc x = PE_+_954510b4 (PE_*_954510b4 x x) x
129More interestingly, consider ``vadd`` which adds corresponding elements
130in a vector of anything numeric:
134 vadd : Num a => Vect n a -> Vect n a -> Vect n a
136 vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
138If we use this on something concrete as follows...
142 test : List Int -> List Int
143 test xs = let xs' = fromList xs in
144 toList $ vadd xs' xs'
146...then in fact, we get a specialised version of ``vadd`` in the
147definition of ``test``, and indeed the specialised version of
152 test : List Int -> List Int
153 test xs = let xs' = fromList xs
154 in PE_toList_888ae67 (PE_vadd_33f98d3d xs' xs')
156Here's the specialised version of ``vadd``:
160 PE_vadd_33f98d3d : Vect n Int -> Vect n Int -> Vect n Int
161 PE_vadd_33f98d3d [] [] = []
162 PE_vadd_33f98d3d (x :: xs) (y :: ys) = ((PE_+_954510b4 x y) ::
163 (PE_vadd_33f98d3d xs ys))
165Note that the recursive structure has been preserved, and the recursive
166call to ``vadd`` has been replaced with a recursive call to the
167specialised version. We've also got the same specialised version of
168``+`` that we had above in ``calc``.
170Specialising Higher Order Functions
171-----------------------------------
173Another case where partial evaluation can be useful is in automatically
174making specialised versions of higher order functions. Unlike type class
175dictionaries, this is not done automatically, but we might consider
176writing ``map`` as follows:
180 my_map : %static (a -> b) -> List a -> List b
182 my_map f (x :: xs) = f x :: my_map f xs
184Then using ``my_map`` will yield specialised versions, for example to
185double every value in a list of ``Int``\ s we could write:
189 doubleAll : List Int -> List Int
190 doubleAll xs = my_map (*2) xs
192This would yield a specialised version of ``my_map``, used in
193``doubleAll`` as follows:
197 doubleAll : List Int -> List Int
198 doubleAll xs = PE_my_map_1f8225c4 xs
200 PE_my_map_1f8225c4 : List Int -> List Int
201 PE_my_map_1f8225c4 [] = []
202 PE_my_map_1f8225c4 (x :: xs) = ((PE_*_954510b4 x 2) :: (PE_my_map_1f8225c4 xs))
204Specialising Interpreters
205-------------------------
207A particularly useful situation where partial evaluation becomes
208effective is in defining an interpreter for a well-typed expression
209language, defined as follows (see the `Idris tutorial, section
2104 <https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
211for more details on how this works):
215 data Expr : Vect n Ty -> Ty -> Type where
216 Var : HasType i gamma t -> Expr gamma t
217 Val : (x : Int) -> Expr gamma TyInt
218 Lam : Expr (a :: gamma) t -> Expr gamma (TyFun a t)
219 App : Lazy (Expr gamma (TyFun a t)) -> Expr gamma a -> Expr gamma t
220 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr gamma a -> Expr gamma
222 If : Expr gamma TyBool -> Expr gamma a -> Expr gamma a -> Expr gamma a
230We can write a couple of test functions in this language as follows,
231using the ``dsl`` notation to overload lambdas; first a function which
232multiplies two inputs:
236 eMult : Expr gamma (TyFun TyInt (TyFun TyInt TyInt))
237 eMult = expr (\x, y => Op (*) x y)
239Then, a function which calculates the factorial of its input:
243 eFac : Expr gamma (TyFun TyInt TyInt)
244 eFac = expr (\x => If (Op (==) x (Val 0))
246 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
248The interpreter's type is written as follows, marking the expression to
249be evaluated as ``%static``:
253 interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
255This means that if we write an Idris program to calculate a factorial by
256calling ``interp`` on ``eFac``, the resulting definition will be
257specialised, partially evaluating away the interpreter:
262 runFac x = interp [] eFac x
264We can see that the call to ``interp`` has been partially evaluated away
269 *interp> :printdef runFac
271 runFac x = PE_interp_ed1429e [] x
273If we look at ``PE_interp_ed1429e`` we'll see that it follows exactly
274the structur of ``eFac``, with the interpreter evaluated away:
278 *interp> :printdef PE_interp_ed1429e
279 PE_interp_ed1429e : Env gamma -> Int -> Int
280 PE_interp_ed1429e (3arg) = \x =>
283 (Delay (PE_interp_b5c2d0ff (x :: (3arg))
284 (PE_interp_ed1429e (x :: (3arg)) (x - 1)) x))
287For the sake of readability, I have simplified this slightly: what you
288will really see also includes specialised versions of ``==``, ``-`` and
289``fromInteger``. Note that ``PE_interp_ed1429e``, which represents
290``eFac`` has become a recursive function following the structure of
291``eFac``. There is also a call to ``PE_interp_b5c2d0ff`` which is a
292specialised interpeter for ``eMult``.
294These definitions arise because the partial evaluator will only
295specialise a definition by a specific concrete argument once, then it is
296cached for future use. So any future applications of ``interp`` on
297``eFac`` will also be translated to ``PE_interp_ed1429e``.
299The specialised version of ``eMult``, without any simplification for
304 PE_interp_b5c2d0ff : Env gamma -> Int -> Int -> Int
305 PE_interp_b5c2d0ff (3arg) = \x => \x1 => PE_*_954510b4 x x1
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