Vincent Balat

Type-Directed Partial Evaluation for the types lambda-calculus with strong binary sums

This page explains how to download and install the normalizer for the lambda-calculus with strong sums described in the paper:
Vincent Balat, Roberto Di Cosmo and Marcelo Fiore,
Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda-Calculus with Sums
POPL 2004

This normalisation tool based on Type-Directed Partial Evaluation (TDPE) allows to normalise lambda-terms with binary sums (written as Objective Caml programs), into a (small) canonical form. For more details, refer to the paper.

Installation

WARNING: A bug in ocaml 3.07 prevents from using the pretty-printer (bug #1891). Please use another version.

Requirements

We are using a modified version of ocaml, with an experimental call/cc control operator. To install, you need:

- ocaml (any version)
- ocaml sources (to compile callcc)
- the source of the normaliser, that you can download here.

Compile callcc

First compile callcc:

- Go to the directory callcc
- Modify the Makefile to set up your paths
- Type make all

Then contruct a toplevel with callcc, for ex:
ocamlmktop -custom -o ocamlcallcc callcc/callcc.cmo callcc/callcc.o

How does it work

Go to the directory of the normaliser, run your toplevel, and use the file load.ml to load the normaliser.

If you use the file loadsr.ml, you will get the traditional TDPE version without let insertion, based on shift and reset, that does not performs all optimizations described in the POPL paper.

The following example shows a typical session. You will find more examples in the file examples.ml of the distribution.

aluminium$ ./ocamlcallcc

        Objective Caml version 3.04

# #cd "/home/pps/balat/tdpe2";;
# #use "load.ml";;
...
# let f x = x;;
val f : 'a -> 'a = 
# normalize (base **-> base) f;;
- : Normal.normal = (fun v0 -> v0)

...

# #use "loadsr.ml";;
...
# let f x = x;;
val f : 'a -> 'a = 
# normalizesr (base **-> base) f;;
- : Normal.normal = (fun v0 -> v0)

Examples

Example 1

# let f x g = match g x with Gauche c -> (fun y -> Gauche y) | _ -> (fun y -> (g x));;

(* with the traditional TDPE (with shift-reset) : *)
normalizesr  (base **-> ((base **-> (sum (base ,base))) **-> ((base **-> (sum (base ,base)))))) f;;
- : Controls2.ans =
(fun v0 v1 -> (match (v1 v0) with
               | Gauche  v2 -> (fun v5 -> Gauche (v5))
               | Droite  v2 -> (fun v3 -> (match (v1 v0) with
                                           | Gauche  v4 -> Gauche (v4)
                                           | Droite  v4 -> Droite (v4))
              ))


(* with our normaliser: *)
normalize  (base **-> ((base **-> (sum (base ,base))) **-> ((base **-> (sum (base ,base)))))) f;;
- : Normal.normal =
(fun v0 v1 -> (match v1 v0 with
               | Gauche  v5 -> (fun v8 -> Gauche (v8))
               | Droite  v6 -> (fun v4 -> Droite (v6)))
              )

For other examples, see the file examples.ml of the distribution.