@@ -0,0 +1,305 @@
1+****************************************
2+Static Arguments and Partial Evaluation
3+****************************************
5+As of version 0.9.15, Idris has support for *partial evaluation* of
6+statically known arguments. This involves creating specialised versions
7+of functions with arguments annotated as ``[static]``.
9+(This is an implementation of the partial evaluator described in `this
11+paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
12+Please refer to this for more precise definitions of what follows.)
14+Partial evaluation is switched on by default. It can be disabled with
15+the ``--no-partial-eval`` flag.
20+Consider 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)
29+This is implemented by recursion on the second argument, and we can
30+evaluate the definition further if the second argument is known, even if
31+the first isn't. For example, we can build a function at the REPL to
32+cube a number as follows:
36+ *pow> \x => my_pow x 3
37+ \x => mult x (mult x (mult x 1)) : Nat -> Nat
41+Note that in the resulting function the recursion has been eliminated,
42+since ``my_pow`` is implemented by recursion on the known argument. We
43+have 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
50+Now, consider the following definition which calculates x^2 + 1:
55+ powFn x = plus (my_pow x (S (S Z))) (S Z)
57+Since the second argument to ``my_pow`` here is statically known, it
58+seems a shame to have to make the recursive calls every time. However,
59+Idris will not in general inline recursive definitions, in particular
60+since they may diverge or duplicate work without some deeper analysis.
62+We can, however, give Idris some hints that here we really would like to
63+create a specialised version of ``my_pow``.
65+Automatic specialisation of ``pow``
66+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68+The 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)
77+When an argument is annotated in this way, Idris will try to create a
78+specialised 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``
81+defined as above, we can see the effect by typing ``:printdef powFn`` at
86+ *pow> :printdef powFn
88+ powFn x = plus (PE_my_pow_3f3e5ad8 x) 1
90+What is this mysterious ``PE_my_pow_3f3e5ad8``? It's a specialised power
91+function where the statically known argument has been specialised away.
92+The name is generated from a hash of the specialised arguments, and we
93+can 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))
101+The ``(0arg)`` is an internal argument name (programmers can't give
102+variable names beginning with a digit after all). Notice also that there
103+is a specialised version of ``fromInteger`` for ``Nat``\ s, since type
104+class dictionaries are themselves a particularly common case of
105+statically known arguments!
107+Specialising Type Classes
108+-------------------------
110+Type class dictionaries are very often statically known, so Idris
111+automatically marks any type class constraint as ``[static]`` and builds
112+specialised versions of top level functions where the class is
113+instantiated. For example, given:
118+ calc x = (x * x) + x
120+If 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
129+More interestingly, consider ``vadd`` which adds corresponding elements
130+in 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
138+If 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
147+definition 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')
156+Here'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))
165+Note that the recursive structure has been preserved, and the recursive
166+call to ``vadd`` has been replaced with a recursive call to the
167+specialised version. We've also got the same specialised version of
168+``+`` that we had above in ``calc``.
170+Specialising Higher Order Functions
171+-----------------------------------
173+Another case where partial evaluation can be useful is in automatically
174+making specialised versions of higher order functions. Unlike type class
175+dictionaries, this is not done automatically, but we might consider
176+writing ``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
184+Then using ``my_map`` will yield specialised versions, for example to
185+double every value in a list of ``Int``\ s we could write:
189+ doubleAll : List Int -> List Int
190+ doubleAll xs = my_map (*2) xs
192+This 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))
204+Specialising Interpreters
205+-------------------------
207+A particularly useful situation where partial evaluation becomes
208+effective is in defining an interpreter for a well-typed expression
209+language, defined as follows (see the `Idris tutorial, section
210+4 <http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
211+for 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
230+We can write a couple of test functions in this language as follows,
231+using the ``dsl`` notation to overload lambdas; first a function which
232+multiplies two inputs:
236+ eMult : Expr gamma (TyFun TyInt (TyFun TyInt TyInt))
237+ eMult = expr (\x, y => Op (*) x y)
239+Then, 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))
248+The interpreter's type is written as follows, marking the expression to
249+be evaluated as ``[static]``:
253+ interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
255+This means that if we write an Idris program to calculate a factorial by
256+calling ``interp`` on ``eFac``, the resulting definition will be
257+specialised, partially evaluating away the interpreter:
262+ runFac x = interp [] eFac x
264+We can see that the call to ``interp`` has been partially evaluated away
269+ *interp> :printdef runFac
271+ runFac x = PE_interp_ed1429e [] x
273+If we look at ``PE_interp_ed1429e`` we'll see that it follows exactly
274+the 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))
287+For the sake of readability, I have simplified this slightly: what you
288+will 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
292+specialised interpeter for ``eMult``.
294+These definitions arise because the partial evaluator will only
295+specialise a definition by a specific concrete argument once, then it is
296+cached for future use. So any future applications of ``interp`` on
297+``eFac`` will also be translated to ``PE_interp_ed1429e``.
299+The 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