All Projects → shonfeder → um-abt

shonfeder / um-abt

Licence: MIT license
An OCaml library implementing unifiable abstract binding trees (UABTs)

Programming Languages

ocaml
1615 projects

Projects that are alternatives of or similar to um-abt

scope-analyzer
simple scope analysis for javascript ASTs
Stars: ✭ 20 (-20%)
Mutual labels:  variables
expandvars
Expand system variables Unix style
Stars: ✭ 17 (-32%)
Mutual labels:  variables
Naming Cheatsheet
Comprehensive language-agnostic guidelines on variables naming. Home of the A/HC/LC pattern.
Stars: ✭ 9,475 (+37800%)
Mutual labels:  variables
hass-variables
Home Assistant variables component
Stars: ✭ 35 (+40%)
Mutual labels:  variables
node-v
🔒 Secure ❄️ Synchronized ⚡️ Realtime ☁️ Cloud 🌈 Native JavaScript Variables & Events
Stars: ✭ 27 (+8%)
Mutual labels:  variables
mkdocs-markdownextradata-plugin
A MkDocs plugin that injects the mkdocs.yml extra variables into the markdown template
Stars: ✭ 48 (+92%)
Mutual labels:  variables
ftor
ftor enables ML-like type-directed, functional programming with Javascript including reasonable debugging.
Stars: ✭ 44 (+76%)
Mutual labels:  unification
pytest-variables
Plugin for providing variables to pytest tests/fixtures
Stars: ✭ 69 (+176%)
Mutual labels:  variables
richvariables
DEPRECATED Allows you to easily use Craft Globals as variables in Rich Text fields
Stars: ✭ 44 (+76%)
Mutual labels:  variables
Cross Env
🔀 Cross platform setting of environment scripts
Stars: ✭ 5,623 (+22392%)
Mutual labels:  variables
ScoreboardStats
Bukkit plugin for customizing the sidebar of the scoreboard feature from minecraft
Stars: ✭ 29 (+16%)
Mutual labels:  variables
ngx-env
Easily inject environment variables into your Angular applications
Stars: ✭ 73 (+192%)
Mutual labels:  variables
envy
Use envy to manage environment variables with your OS keychain
Stars: ✭ 23 (-8%)
Mutual labels:  variables
py better exchook
nice Python exception hook replacement
Stars: ✭ 35 (+40%)
Mutual labels:  variables
godump
Dumps information about a variable Like var_dump() in php.
Stars: ✭ 54 (+116%)
Mutual labels:  variables
AI physicist
AI Physicist, a paradigm with algorithms for learning theories from data, by Wu and Tegmark (2019)
Stars: ✭ 23 (-8%)
Mutual labels:  unification
vue-global-var
Reactive global variable can be sharable between components
Stars: ✭ 21 (-16%)
Mutual labels:  variables
programming-language-theory
Programming Language Research, Applied PLT & Compilers
Stars: ✭ 53 (+112%)
Mutual labels:  plt
terraform-digitalocean-variables
List of all available DigitalOcean droplet image distributions, one click applications, regions and sizes.
Stars: ✭ 26 (+4%)
Mutual labels:  variables
environment
🌳 Environment variable configuration for Node.js made easy.
Stars: ✭ 12 (-52%)
Mutual labels:  variables

um-abt

build

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:

  1. It should be correct.
  2. It should be well tested, to ensure its correctness.
  3. It should be easy to use.
  4. It should be well documented.

Features

This ABT library has two distinctive (afaik) features:

  1. 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.

  2. 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 [email protected]: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 the Abt.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 using ppx_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):

    The crucial idea is that any use of an identifier should be understood as a reference, or abstract pointer, to its binding. (PFPL, 2nd ed., p. 6)

  • 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.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].