yallop/metaocaml-letrec

flexible 'let rec' generation for MetaOCaml

metaocaml-letrec: flexible 'let rec' generation

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.

Installation

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

Further reading

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

metaocaml-letrec's Issues

Possible to setup metaocaml with utop?

Hi @yallop

I was wondering if it's somehow possible to have the same kind of utop support of metaocaml as well.

I use the ocaml layer in spacemacs and since by default utop emacs mode is not working for spacemacs, I'm exploring theocaml toplevel - which seems an absolute minimum repl to be sure.

Is there a way, I could have a more interactive experience with metaocaml ?

Unable to install metaocaml

Hi @yallop

I am trying to install the metaocaml variant to try out this package but opam isn't responding as per the ReadMe.md instructions.

I reached this repo via the following paper https://www.cl.cam.ac.uk/~jdy22/papers/generating-mutually-recursive-definitions.pdf

First off, I'm only able to run opam when using sudo as mentioned here ocaml/opam-repository#13111 (comment)

Abhinavs-MacBook-Pro:~ eklavya$ sudo opam switch 4.07.1+BER
[WARNING] Running as root is not recommended
# Run eval $(opam env) to update the current shell environment
Abhinavs-MacBook-Pro:~ eklavya$ eval $(opam config env)
Abhinavs-MacBook-Pro:~ eklavya$ eval $(opam env)
Abhinavs-MacBook-Pro:~ eklavya$ ocaml
bash: ocaml: command not found
Abhinavs-MacBook-Pro:~ eklavya$ opam env
OPAM_SWITCH_PREFIX='/Users/eklavya/.opam/4.07.1+BER'; export OPAM_SWITCH_PREFIX;

How can I make all of this work?

Add support for BER N111 (4.11.1+BER in opam)