05 April 2012

Fixed-Point Magic: Successive Recursive Calls

A brief summary of the Y-combinator trick, and an unusual use.

You may be familiar with the Y combinator and its sexy uses in functional programming. The standard examples of use are logging and caching. Let's summarize how the trick works. Given a recursive function $f:a\to b$, you rewrite it into a non-recursive function $f':(a\to b)\to(a\to b)$: The body of $f'\;f$ (that is, $f'$ applied to its first argument which we name $f$) looks exactly the same as the body of $f$. At this point, types are already long, so I'll write $t^\circ$ for $t\to t$. For example the type of $f'$ is $(a\to b)^\circ$. The Y combinator has the type $\forall\alpha\beta,\,(\alpha\to\beta)^\circ\to(\alpha\to\beta)$. In words, Y takes a function like $f'$ and ‘ties the knot’ to give us back $f$. Before tying the knot, however, you may apply to $f'$ any number of transformers, which are functions of type $(a\to b)^{\circ\circ}$. Roughly, each transformer pre-processes the argument and post-processes the result.

Here is an example.

let rec y f x = f (y f) x
let fib' fib n = if n < 2 then n else fib (n - 1) + fib (n - 2)
let p_int x = printf "%d\n" x
let log p f' f n = p n; f' f n
let fib = y (log p_int fib')

The call fib 3 prints the following:

3
1
2
0
1

But suppose you want to print the call graph.

init -> 3
3 -> 1
3 -> 2
2 -> 0
2 -> 1

To do so, a transformer needs access to the current value of the argument, but also to the previous value. We will use a combinator successive of type $$ \forall\alpha\beta\gamma,\;(\alpha\to\gamma)\to(\alpha\to\beta)^\circ\to(\gamma\times\alpha\to\beta)^\circ $$ It transforms an untied function of type $(a\to b)^\circ$ into an untied function of type $(c\times a\to b)^\circ$, using a helper of type $a\to c$.

let successive g f' f (x, y) = f' (fun z -> f (g y, z)) y
let p_string_int (s, n) = printf "%s -> %d\n" s n
let fib = y (log p_string_int (successive string_of_int fib'))
let _ = fib ("init", 3)

Let's break down the types involved in the second to last line, because they can get long and may be hard to track in one's head.

fib' : (int -> int) -> (int -> int)
string_of_int : int -> string
successive :
  (int -> string)
  -> ((int -> int) -> (int -> int))
  -> (string * int -> int) -> (string * int -> int)
successive string_of_int fib' :
  (string * int -> int) -> (string * int -> int)
p_string_int : string * int -> unit
log :
  (string * int -> unit)
  -> ((string * int -> int) -> (string * int -> int))
  -> (string * int -> int) -> (string * int -> int)
log p_string_int (successive string_of_int fib') :
  (string * int -> int) -> (string * int -> int)
y :
  ((string * int -> int) -> (string * int -> int))
  -> (string * int -> int)
fib : string * int -> int

No comments:

Post a Comment

Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.