um-abt
Table of Contents
Overview
um-abt
is an OCaml library implementing abstract binding trees (ABTs)
exhibiting the properties defined in Robert
Harper's Practical Foundations for
Programming Labguages (PFPL).
Documentation
Aims
This library aims for the following qualities:
It should be correct.
It should be well tested, to ensure its correctness.
It should be easy to use.
It should be well documented.
Features
This ABT library has two distinctive (afaik) features:
The library augments the binding functionality of the ABT approach with
unification modulo ɑ-equivalence. We might therefore describe this
library as an implementation of unifiable abstract binding trees (or
UABTs): where ABTs provide a general and reusable system for variable
binding, UABTs add a general and reusable system for nominal unification.Unification is lovely and not used nearly enough, imo.
The library implements variable binding via (what we might call) binding by
reference; i.e., variable binding is recorded in the pointer structure of
by way of "immutable" reference cells. This is somewhat of an experiment:
being unaware of other implementations using this approach, I worked out the
details as I went. So far, it seems to have yielded [trivial ɑ-equivalence
and substitution algorithms, and enabled nominal unification][], without
requiring any bureaucratic fiddling with renaming, variable permutations, or
fresh variables.
Caveat emptor: I am not an academic PLT researcher and this library has not
yet been used extensively.
Installation
The latest released version can be installed with
opam:
opam install um-abt
To install the head of development
opam pin git@github.com:shonfeder/um-abt.git
Synopsis
The following short examples help illustrate use of the library. For more
extensive examples, see
test/example/example.ml.
An ABT for the λ-calculus
Here is a short example showing a naive implementation of the untyped lambda
calculus using um-abt
.
ABTs representing the syntax of a language are produced by applying theAbt.Make
functor to a module implementing the Operator
specification.
module Syntax = struct
(* Define the usual operators, but without the variables, since we get those free *)
module O = struct
type 'a t =
| App of 'a * 'a
| Lam of 'a
[@@deriving eq, map, fold, sexp]
let to_string : string t -> string = function
| App (l, m) -> Printf.sprintf "(%s %s)" l m
| Lam abs -> Printf.sprintf "(λ%s)" abs
end
(* Generate the syntax, which will include a type [t] of the ABTs over the operators **)
include Abt.Make (O)
(* Define some constructors to ensure correct construction *)
let app m n : t =
(* [op] lifts an operator into an ABT *)
op (App (m, n))
let lam x m : t =
(* ["x" #. scope] binds all free variables named "x" in the [scope] *)
op (Lam (x #. m))
end
The generated ABT will have the following form:
type t = private
| Var of Abt.Var.t
| Bnd of Abt.Var.binding * t
| Opr of t O.t
Most of the values required by the Operator
specification can be derived usingppx_deriving
. So all that is
usually required is to define a datatype representing the operators and their
arities.
After the ABT is generated However, it is recommended that one also define constructors making it
more convenient and safer to construct terms of the language.
The private
annotation indicates that you can use pattern matching to
deconstruct the ABT, but you cannot construct new values without using the
supplied combinators. This ensures essential invariants are preserved. E.g., it
is impossible to construct a binding in which the expected variables are not
bound in the term in scope.
For a more perspicuous view of our produce, let's define the SKI
combinators and see what
they look like when printed in the usual notation:
(* [v x] is a free variable named "x" *)
let x, y, z = Syntax.(v "x", v "y", v "z")
let s = Syntax.(lam "x" (lam "y" (lam "z" (app (app x y) (app y z)))))
let k = Syntax.(lam "x" (lam "y" x))
let i = Syntax.(lam "x" x)
let () =
assert (Syntax.to_string s = "(λx.(λy.(λz.((x y) (y z)))))");
assert (Syntax.to_string k = "(λx.(λy.x))");
assert (Syntax.to_string i = "(λx.x)");
Note that equality between ABTs is defined in terms of ɑ-equivalence, so we can
define the i
using any variable, and it will be equivalent:
let () =
assert Syntax.(equal i (lam "y" y))
Now let's define reduction, using the API provided by our generated Syntax
.Syntax
modules expose private
value constructors, which provide a
pattern-matching based interface for destructuring ABTs, but prevents
constructing new ABTs directly. This gives us the convenience of a pattern
matching API without compromising the integrity of the ABT representation by
allowing ill-formed structures.
open Syntax
let rec eval : t -> t =
fun t ->
match t with
| Opr (App (m, n)) -> apply (eval m) (eval n)
(* No other terms can be evaluated *)
| _ -> t
and apply : t -> t -> t =
fun m n ->
match m with
| Bnd (bnd, t) -> subst bnd ~value:n t
| Opr (Lam bnd) -> eval (apply bnd n)
(* otherwise the application can't be evaluated *)
| _ -> app m n
Finally, let's illustrate the correctness of our implementation with a few
simple evaluations, demonstrating that our SKI combinators behave as expected:
let () =
(* Let equality be ɑ-equivalence on our syntax for the following examples *)
let (=) = Syntax.equal in
let open Syntax in
assert (eval (app i x) = x);
assert (eval (app (app k x) y) = x);
assert (eval (app (app (app s x) y) z) = (app (app x y) (app y z)))
(See
https://en.wikipedia.org/wiki/SKI_combinator_calculus#Informal_description for
reference.)
Unification over λ-calculus terms
The ABTs produced by applying the Abt.Make
functor to an Operator
implementation support first-order, syntactic unification modulo ɑ-equivalence.
Unification is (currently) limited to first-order, because there is no support
for variables standing for operators.Unification is (currently) syntactic, because we do not perform any evaluation
to determine if two ABTs can be unified.Unification is modulo ɑ-equivalence, because two ɑ-equivalent ABTs are
considered equal during unification.
let () =
let open Syntax in
(* The generated [Syntax] module includes a [Unification] submodule
- the [=?=] operator checks for unifiability
- the [=.=] operator gives an [Ok] result with the unified term, if its operands unify,
or else an [Error] indicating why the unification failed
- the [unify] function is like [=.=], but it also gives the substitution used to produce
a unified term *)
let ((=?=), (=.=), unify) = Unification.((=?=), (=.=), unify) in
(* A free variable will unify with anything *)
assert (v "X" =?= s);
(* Again, unification is modulo ɑ-equivalence *)
assert (lam "y" (lam "x" y) =?= lam "x" (lam "y" x));
(* Here we unify the free variable "M" with the body of the [k] combinator,
note that the nominal unification is modulo bound variables: *)
let unified_term = (lam "z" (v "M") =.= k) |> Result.get_ok in
assert (to_string unified_term = "(λz.(λy.z))");
(* The substitution allows retrieval the bound values of the free variables *)
let _, substitution = unify (lam "x" (v "M")) k |> Result.get_ok in
assert (Unification.Subst.to_string substitution = "[ M -> (λy.x) ]")
Additional References
Harper explicitly connects binding scope with pointers in PFPL (tho I have not
seen another functional implementation that takes this connection literally):I discussed the idea of using
ref
cells to track binding scope in
conversation with Callan McGill, and the representation of free and bound
variables was influenced by his post "Locally
Nameless".My initial implementation of an ABT library was informed by Neel
Krishnaswami's post on
ABTs.
There are still some aspects of that approach that show up here.I consulted Christian Urban's paper
Nominal Unification Revisited and
Urban, Pitts, and Gabby's Nominal
Unification for guidance on the
harrier bits of unification modulo ɑ-equivalence, tho this library does not
currently take advantage of the strategy of nominal permutations described
there.
sha256=9472873b4f485ff1c169d950488133c79efb4b00b757526bfb14a2f043a0480f
sha512=e3ea3990177778ae109082bea0b952b760b4fc9a243f0321367d2927061e3766c0d99679c5e4b13f89532b22ad4993c34f91b625ec40e07f113b9812521f91f4
with-doc
with-test & >= "1.10.1"
with-test & >= "0.2.0"
with-test & >= "0.17"
>= "0.2.0"
>= "v0.14.3"
>= "5.2.1"
>= "v0.14.1"
>= "v0.14.0"
>= "0.7.0"
>= "2.8"