@@ -0,0 +1,305 @@
1+****************************************
2+Static Arguments and Partial Evaluation
3+****************************************
4+
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]``.
8+
9+(This is an implementation of the partial evaluator described in `this
10+ICFP 2010
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.)
13+
14+Partial evaluation is switched on by default. It can be disabled with
15+the ``--no-partial-eval`` flag.
16+
17+Introductory Example
18+--------------------
19+
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):
22+
23+::
24+
25+ my_pow : Nat -> Nat -> Nat
26+ my_pow x Z = 1
27+ my_pow x (S k) = mult x (my_pow x k)
28+
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:
33+
34+::
35+
36+ *pow> \x => my_pow x 3
37+ \x => mult x (mult x (mult x 1)) : Nat -> Nat
38+ *pow> it 3
39+ 27 : Nat
40+
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:
44+
45+::
46+
47+ *pow> \x => my_pow 2 x
48+ \x => my_pow 2 x : Nat -> Nat
49+
50+Now, consider the following definition which calculates x^2 + 1:
51+
52+::
53+
54+ powFn : Nat -> Nat
55+ powFn x = plus (my_pow x (S (S Z))) (S Z)
56+
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.
61+
62+We can, however, give Idris some hints that here we really would like to
63+create a specialised version of ``my_pow``.
64+
65+Automatic specialisation of ``pow``
66+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
67+
68+The trick is to mark the statically known arguments with the
69+``[static]`` flag:
70+
71+::
72+
73+ my_pow : Nat -> [static] Nat -> Nat
74+ my_pow k Z = 1
75+ my_pow k (S j) = mult k (my_pow k j)
76+
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
82+the REPL:
83+
84+::
85+
86+ *pow> :printdef powFn
87+ powFn : Nat -> Nat
88+ powFn x = plus (PE_my_pow_3f3e5ad8 x) 1
89+
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:
94+
95+::
96+
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))
100+
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!
106+
107+Specialising Type Classes
108+-------------------------
109+
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:
114+
115+::
116+
117+ calc : Int -> Int
118+ calc x = (x * x) + x
119+
120+If we print this definition, we'll see a specialised version of ``+`` is
121+used:
122+
123+::
124+
125+ *petest> :printdef calc
126+ calc : Int -> Int
127+ calc x = PE_+_954510b4 (PE_*_954510b4 x x) x
128+
129+More interestingly, consider ``vadd`` which adds corresponding elements
130+in a vector of anything numeric:
131+
132+::
133+
134+ vadd : Num a => Vect n a -> Vect n a -> Vect n a
135+ vadd [] [] = []
136+ vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
137+
138+If we use this on something concrete as follows...
139+
140+::
141+
142+ test : List Int -> List Int
143+ test xs = let xs' = fromList xs in
144+ toList $ vadd xs' xs'
145+
146+...then in fact, we get a specialised version of ``vadd`` in the
147+definition of ``test``, and indeed the specialised version of
148+``toList``:
149+
150+::
151+
152+ test : List Int -> List Int
153+ test xs = let xs' = fromList xs
154+ in PE_toList_888ae67 (PE_vadd_33f98d3d xs' xs')
155+
156+Here's the specialised version of ``vadd``:
157+
158+::
159+
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))
164+
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``.
169+
170+Specialising Higher Order Functions
171+-----------------------------------
172+
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:
177+
178+::
179+
180+ my_map : [static] (a -> b) -> List a -> List b
181+ my_map f [] = []
182+ my_map f (x :: xs) = f x :: my_map f xs
183+
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:
186+
187+::
188+
189+ doubleAll : List Int -> List Int
190+ doubleAll xs = my_map (*2) xs
191+
192+This would yield a specialised version of ``my_map``, used in
193+``doubleAll`` as follows:
194+
195+::
196+
197+ doubleAll : List Int -> List Int
198+ doubleAll xs = PE_my_map_1f8225c4 xs
199+
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))
203+
204+Specialising Interpreters
205+-------------------------
206+
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):
212+
213+::
214+
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
221+ Expr gamma c
222+ If : Expr gamma TyBool -> Expr gamma a -> Expr gamma a -> Expr gamma a
223+
224+ dsl expr
225+ lambda = Lam
226+ variable = Var
227+ index_first = stop
228+ index_next = pop
229+
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:
233+
234+::
235+
236+ eMult : Expr gamma (TyFun TyInt (TyFun TyInt TyInt))
237+ eMult = expr (\x, y => Op (*) x y)
238+
239+Then, a function which calculates the factorial of its input:
240+
241+::
242+
243+ eFac : Expr gamma (TyFun TyInt TyInt)
244+ eFac = expr (\x => If (Op (==) x (Val 0))
245+ (Val 1)
246+ (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
247+
248+The interpreter's type is written as follows, marking the expression to
249+be evaluated as ``[static]``:
250+
251+::
252+
253+ interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
254+
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:
258+
259+::
260+
261+ runFac : Int -> Int
262+ runFac x = interp [] eFac x
263+
264+We can see that the call to ``interp`` has been partially evaluated away
265+as follows:
266+
267+::
268+
269+ *interp> :printdef runFac
270+ runFac : Int -> Int
271+ runFac x = PE_interp_ed1429e [] x
272+
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:
275+
276+::
277+
278+ *interp> :printdef PE_interp_ed1429e
279+ PE_interp_ed1429e : Env gamma -> Int -> Int
280+ PE_interp_ed1429e (3arg) = \x =>
281+ boolElim (x == 0)
282+ (Delay 1)
283+ (Delay (PE_interp_b5c2d0ff (x :: (3arg))
284+ (PE_interp_ed1429e (x :: (3arg)) (x - 1)) x))
285+
286+
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``.
293+
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``.
298+
299+The specialised version of ``eMult``, without any simplification for
300+readability, is:
301+
302+::
303+
304+ PE_interp_b5c2d0ff : Env gamma -> Int -> Int -> Int
305+ PE_interp_b5c2d0ff (3arg) = \x => \x1 => PE_*_954510b4 x x1