In typed MetaML-based systems such as MetaOCaml it is difficult or impossible to generate mutually-recursive binding groups whose size is not known in advance. For example, suppose (following an example of Neil Jones expounded by Oleg) that you want to specialize the Ackermann function
let rec ack m n =
if m = 0 then n 1 else
if n = 0 then ack (m-1) 1 else
ack (m-1) (ack m (n-1))
with the first argument equal to 2
. Ideally, you might like to generate the following code, with three mutually recursive bindings and all the recursive calls specialized:
let rec ack_2 n = if n = 0 then ack_1 1 else ack_1 (ack_2 (n-1))
and ack_1 n = if n = 0 then ack_0 1 else ack_0 (ack_1 (n-1))
and ack_0 n = n 1
With metaocaml-letrec
you can generate exactly that code, modulo naming, by annotating the original definition of ack
as follows (and passing the argument 2
):
let%staged rec ack m =
.< fun n -> .~(if m = 0 then .<n 1>. else
.< if n = 0 then .~(ack (m-1)) 1 else
.~(ack (m-1)) (.~(ack m) (n-1)) >.)>.
and, in general, ack n
will generate a let rec
group of n 1
bindings.
More generally, metocaml-letrec
treats a let rec
binding as an indexed family, where the argument to the generating function is the index. In the ack
example, the index m
is a simple integer; in general it may be a richer object, making it possible to generate arbitrary patterns of recursion, including
- nested let rec bindings
- polymorphic recursion
- recursion with non-function values
- recursion where the bindings have different types
and many more examples.
metaocaml-letrec
works on various versions of BER MetaOCaml, which are available via OPAM
:
opam switch install 4.14.1 BER
eval $(opam env)
Within this 4.14.1 BER
switch the metaocaml-letrec
package can be installed as follows:
opam remote add metaocaml git https://github.com/metaocaml/metaocaml-opam.git
opam install letrec
The following paper has more details about the design and implementation of metaocaml-letrec
:
Generating mutually recursive definitions
Jeremy Yallop and Oleg Kiselyov
PEPM 2019