call/cc
\x -> x x
cannot even be
assigned any
simple type. Practical typed languages like OCaml and Haskell have
enough features to write the fix-point combinator without resorting to
the built-in recursive binding. In fact, one can write the fix-point
combinator in these languages in quite a few different ways.
The code below demonstrates all the different ways to express the fully polymorphic fix-point combinator in OCaml: from banal
to advanced. Our approach is explicitly based on
self-application. Most of the code focuses on the emulation of (equi-)
recursive types via iso-recursive types. We also explore
equi-recursive types, explicit ones and those inherent in delimited
continuations underlying mutations or exceptions. Along the way we
describe two lesser-known expressions of the fix-point combinator: via
mutations (see FixReferenceA
in the code) and exceptions.
Some of the ML techniques, such as using iso-recursive data types
to define fix
, easily transfer to Haskell. The
side-effecting approaches (e.g., relying on exceptions) do not work so
well if our goal is to write the pure fix
, rather than
the monadic mfix
. Surprisingly, ST
reference
cells let us write the pure fix
, if we use
the lazy ST
monad. Type classes and type families offer a
Haskell-specific way to express the fix-point combinator.
Fix.hs [3K]
Defining the fix-point combinator in Haskell without the value recursion
In the literature a polyvariadic fix-point combinator is often presented using "...", or ellipsis. For example,
(letrec ((f1 e1) (f2 e2) ... (fn en) ) e)is schematically represented via the explicit fix-point as
(let ((fs (Y* (lambda (f1 f2 ... fn) e1) ... (lambda (f1 f2 ... fn) en)))) (apply (lambda (f1 f2 ... fn) e) fs))Surely the mutual fixed-point combinator can be written as a proper lambda-term, without resorting to the meta-language operation, ellipsis. We demonstrate such a lambda term, the simplest so far.
We start by recalling how ordinary general recursion is represented
via the ordinary fix-point combinator such as Y
. A recursive
function like fact
:
let rec fact : int -> int = fun n -> if n <= 0 then 1 else n * fact (n-1)first has to be re-written in a so-called `open recursion style', with the explicit argument for the recursive occurrence:
let open_fact : (int -> int) -> int -> int = fun self n -> if n <= 0 then 1 else n * self (n-1)
This function is no longer recursive. The fix-point combinator
val fix : (('a->'b) -> ('a->'b)) -> ('a->'b)then ties the recursive knot:
fix open_fact;; (* - : int -> int = <fun> *) fix open_fact 5;; (* - : int = 120 *)
We now generalize to mutual recursion, on the familiar example of determining if a natural number is even or odd:
let rec even : int -> bool = fun n -> n = 0 || odd (n-1) and odd : int -> bool = fun n -> n <> 0 && even (n-1)The definition looks like two clauses of a single function, which we call
evod
:type idx = int let rec evod : idx -> int -> bool = function | 0 -> fun n -> n = 0 || evod 1 (n-1) | 1 -> fun n -> n <> 0 && evod 0 (n-1) let even = evod 0 and odd = evod 1The first argument (of type
idx
, integer for now) indexes the clauses.
Since evod
is an ordinary recursive function, quite like fact
,
we re-write it in the open recursion stylelet open_evod : ((idx -> int -> bool) as 't) -> 't = fun self -> function | 0 -> fun n -> n = 0 || self 1 (n-1) | 1 -> fun n -> n <> 0 && self 0 (n-1)and then apply the ordinary fix-point combinator:
let evod = fix open_evod (* val evod : idx -> int -> bool = <fun> *) let even = evod 0 and odd = evod 1 (* val even : int -> bool = <fun> *) (* val odd : int -> bool = <fun> *)
We thus obtain that the polyvariadic fix-point combinator
let fix_poly_v1 : ('t ->'t) -> ((idx -> 'a -> 'b) as 't) = fixis just an instance of the ordinary fix-point combinator. It seems we are done. However, the interface of
fix_poly_v1
is cumbersome,
requiring a function like open_evod
with the explicitly indexed
clauses. Recursive applications have to apply the index, which is
error-prone and inefficient. There is another problem: all mutually
recursive clauses are restricted to be of the same type. We lift that
restriction at the end.We now derive a mutual fix-point combinator with the better interface and efficiency. We wish the fix-point combinator took a list of functions in the open recursion style, returning the list of functions with their knots tied-up. Ideally, the running example should look like
let [even;odd] = let open_even [even;odd] = fun n -> n = 0 || odd (n-1) and open_odd [even;odd] = fun n -> n <> 0 && even (n-1) in fix_poly [open_even;open_odd]Hence the polyvariadic fix-point combinator should have the following type
val fix_poly : (('a -> 'b) list -> ('a -> 'b)) list -> ('a -> 'b) listWe develop exactly such combinator. It seems easy since
fix_poly_v1
is
straightforward to adapt to the above signature. The key point is that
a total function idx -> t
with some result type t
and the domain [0..n-1]
for idx
is isomorphic to the n
-element t list
. Writing
out the conversion between the two representations explicitly gives us:let fix_poly_temp : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list = fun l -> let n = List.length l in let clause self idx = (List.nth l idx) (List.map self (iota n)) in List.map (fix_poly_v1 clause) (iota n)
where iota n
produces a list of integers 0
through n-1
. This
combinator has two problems: divergence and inefficiency.
The former is easy to fix with the appropriate eta-expansion
let fix_poly_v2 : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list = fun l -> let n = List.length l in let clause self idx x = (List.nth l idx) (List.map self (iota n)) x in let tied idx x = fix clause idx x in List.map tied (iota n)
giving us a polyvariadic fix-point combinator with the desired
interface. List.nth
and iota
strongly remind of Queinnec's NfixN2
, described in his book ``LISP In Small Pieces''. However, not
only List.nth
(in Scheme, list-ref
) is inefficient (indexing a
list requires its traversal and hence is not constant time), it is
also aesthetically displeasing. Ideally, the list of clauses should be
handled as an abstract collection, using only operations like fold or
map rather than random-access List.nth
. It would be easy then to
generalize to other collections, such as tuples.
We now improve the efficiency of fix_poly_v2
, getting rid of List.nth
.
The starting point is the simpler fix_poly_temp
: we can always fix
the divergence later, with eta-expansion. Let fl
be fix_poly_temp l
for some appropriate list l
and let clause = fun self idx -> (List.nth l idx) (List.map self (iota n))
.
We calculate
fl === fix_poly_temp l === map (fix clause) (iota n) {fixpoint} === map (clause (fix clause)) (iota n) {inline the first clause, beta-reduce} === map (fun idx -> List.nth l idx (map (fix clause) (iota n))) (iota n) {Recall, map (f . g) l === map f . map g l, and map (fun idx -> List.nth l idx) (iota (List.length l)) === l } === map (fun li -> li (map (fix clause) (iota n))) l === {recall what fix_poly_temp l is} === map (fun li -> li (fix_poly_temp l)) l
The result shows that fix_poly_temp l
is an ordinary fix-point, of fun self -> map (fun li -> li self) l
. The result is immediately usable
in Haskell. In OCaml, we have to introduce
a few eta-expansions to prevent premature looping.
let fix_poly : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list = fun l -> fix (fun self l -> List.map (fun li x -> li (self l) x) l) lThis combinator has the desired interface and efficiency. We have achieved our goal.
The combinator fix_poly
is straightforward to translate into Scheme.
After inlining the definition of the ordinary fix-point combinator
and simplifying, we obtain the following expression for the
polyvariadic fix-point combinator. It is notably simpler than
the polyvariadic combinators by Queinnec and Goldberg.
(define (Y* . l) ((lambda (u) (u u)) (lambda (p) (map (lambda (li) (lambda x (apply (apply li (p p)) x))) l))))
Compared to the OCaml version, the functions to obtain the mutual fix-point of do not have to have the same number of arguments (the same arity). The accompanying code shows an example.
The combinator fix_poly
translates to Haskell trivially. Since Haskell
is non-strict, no eta-expansions are needed. The result is a one-liner:
fix_poly:: [[a]->a] -> [a] fix_poly fl = fix (\self -> map ($ self) fl) where fix f = f (fix f) test1 = (map iseven [0..5], map isodd [0..5]) where [iseven, isodd] = fix_poly [fe,fo] fe [e,o] n = n == 0 || o (n-1) fo [e,o] n = n /= 0 && e (n-1)
The type of fix_poly
points out the remaining problem: all mutually
dependent clauses are restricted to the same type. This is a serious limitation.
The type of fix_poly
has a curious structure, which shows the way out,
through the second-order Functor
:
class Functor2 c where fmap2 :: (forall a. c1 a -> c2 a) -> c c1 -> c c2for collections
c
indexed by a type constructor c1
. Lists are such
collections, and so are tuples:newtype Id a = Id{unId :: a} newtype P3 a1 a2 a3 c = P3 (c a1, c a1, c a3) instance Functor2 (P3 a1 a2 a3) where fmap2 f (P3 (x,y,z)) = (P3 (f x, f y, f z))The general polyvariadic fix-point combinator takes then the following form:
fix_gen_poly:: Functor2 c => c ((->) (c Id)) -> c Id fix_gen_poly fl = fix (\self -> fmap2 (\x -> Id (x self)) fl) where fix f = f (fix f)The accompanying code shows an example of its use.
In conclusion: we have developed the simplest to date polyvariadic combinator
for mutual fix-point: \l -> fix (\self -> map ($ self) l)
.
PolyY.hs [2K]
Several examples of fix_poly in Haskell
Polyvariadic Y: a mutually least fixpoint combinator for several terms
A message posted on the Haskell Cafe mailing list on Oct 27, 2003.
Mayer Goldberg: A Variadic Extension of Curry's Fixed-Point Combinator
Higher-Order and Symbolic Computation, v18, N3-4, pp 371-388, 2005
As common (see Goldberg 2005 for references), we call a closed lambda-term F
a fix-point combinator if the following equation holds for any term e
:
F e =*= e (F e)where
(=*=)
is the beta-eta equality. That is, two lambda-terms M
and N
are beta-eta equal iff there exists a term L
to which they both reduce
in 0 or more steps. Even divergent terms (which have no normal form) can
be determined equal. The well-known Y
combinator is one example of
the fix-point combinator. There are infinitely many more. For instance,
if F
is a fix-point combinator, so is F . I
, where I
is the identity
and (.)
is the functional composition. Less trivially, if F
is a fix-point
combinator and G = \f g e x -> e (f (g e))
, then F . F (G F)
is a fix-point
combinator.The set of fix-point combinators, albeit infinite, is effectively countable, or recursively enumerable. There exists an effective process, a program, that produces all fix-point combinators one by one, without duplicates.
For the proof, we take the inspiration from the well-known demonstration that the set of all halting programs (or, all normalizable lambda-terms) is recursively enumerable. This fact does not imply that termination or normalization are decidable since the complement set, of non-terminating terms is not recursively enumerable. The recursive enumerability of normalizable terms can be demonstrated as a simple non-deterministic program:
list_normalizable :: MonadPlus m => m Exp list_normalizable = do term <- a_term check_normalization term return term check_normalization :: MonadPlus m => Exp -> m () check_normalization term = check_NF term `mplus` (reduce_one_step term >>= check_normalization) where check_NF term = if is_normal_form term then return () else mzeroHere
a_term :: MonadPlus m => m Exp
non-deterministically generates
a lambda-term (represented as a value of the data type Exp
). One
can always write such a procedure since the set of all lambda-terms
is recursively enumerable. The total function is_normal_form :: Exp -> Bool
tests if a term is in normal form, and a function reduce_one_step :: MonadPlus m => Exp -> m Exp
non-deterministically picks a redex and contracts it, returning the reduced
term. Both operations can be done in finite time.
The decision tree for the list_normalizable
program is infinite.
Normalizable terms are at the leaves of the tree, at a finite distance
from the root: By definition, a term is normalizable if it can be reduced
to a normal form in a finite number of steps. A complete search procedure
(such as breadth-first search) will traverse the tree, listing all leaves
in some order.
The second key idea of our proof of the recursive enumerability of fix-point
combinators is that the equality of two lambda-terms can be confirmed in finite
time. Given two terms M
and N
, we non-deterministically apply
0 or more reduction steps to M
and 0 or more reduction steps to N
.
If M
and N
are beta-eta-equal, the results will be identical modulo
alpha-renaming. This procedure does not imply that beta-eta-equality
is decidable since the disequality of terms cannot be, in general, established
in finite time. Putting these facts together, we obtain the proof:
non-deterministically generate a closed term F
, and check
that F e
is beta-eta-equal to e (F e)
where e
is a fresh variable.
The enclosed code is the complete proof -- the program that produces all fix-point combinators one-by-one. Here is the key part:
list_fix :: MonadPlusOnce m => m Exp list_fix = do term <- a_term let fixe = A term e once $ check_equal fixe (A e fixe) return term
As before, a_term
non-deterministically picks a lambda-term, in
deBruijn notation. The function check_equal :: MonadPlus m => Exp -> Exp -> m ()
checks if two
terms beta-eta equal. Two terms may be equal in more than one way; any
one way is sufficient. The search combinator once
prunes the further,
redundant search once the equality has been confirmed.
EnumFix.hs [7K]
Enumerating all fix-point combinators
(define (Y f) ((lambda (u) (u u)) (lambda (p) (lambda (x) ((f (p p)) x)))))In contrast, the self-application combinator, typically called
delta
,
expresses the explicit fix-point quite more concisely:(define delta (lambda (u) (u u))) (define (fact-nr self) ; non-recursive! (lambda (n) (if (zero? n) 1 (* n ((self self) (- n 1)))))) ((delta fact-nr) 5) ; ==> 120
We now describe the simple inter-relationship between the Y
combinator
and the self-application combinator that we call U
:
(define U (lambda (f) (lambda (x) (f (x x)))))Clearly,
delta
is a particular case of U
, namely, U
applied to
the identity function. The combinator U
can express a
fix-point of any term. Indeed, keeping in mind the reduction rule
of the combinatorU f x ==> f (x x)we immediately see that for any term
e
:(U e) (U e) ==> e ((U e) (U e))Since
S U U e
reduces to (U e) (U e)
, we obtain a concise expression
for the fix-point combinator: S U U
. It is easy to see that S U U
is beta-eta-equal to the familiar Y
.
The combinator U
can be expressed in terms of S
, K
and I
: U = S (CSC) (KI)
, where C = S (KS) K
is the composition combinator.
Indeed, keeping in mind the re-writing rules of the combinator calculus
S f g x ==> f x (g x) K c x ==> c I x ==> x C f g x ==> f (g x)we see
U f x = S (CSC) (KI) f x ==> C S C f (K I f) x ==> S (C f) I x ==> C f x (I x) ==> f (x x)
Jon Fairbairn pointed out in a private message that the above explanation is essentially the insight behind Turing's fixed point combinator.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML