Gagallium

We can now demonstrate the Fix library, used to compute arbitrary fixpoints, by implementing variance computation for the toy type system of our first post.

Getting Fix

Fix is available in OPAM, so obtaining it is as simple as:

opam install fix

The following command-line will compile a test file and run the resulting program:

ocamlfind ocamlc -package fix -linkpkg test.ml && ./a.out

Some definitions

We first need to define what is variance, as well as the various operations (negation, composition).

type variance =
  | Inv
  | Co
  | Contra
  | Bi

let join a b =
  match a, b with
  | Inv, _
  | _, Inv ->
      Inv
  | Bi, x
  | x, Bi ->
      x
  | x, y ->
      if x = y then
        x
      else
        Inv
;;

let minus = function
  | Inv -> Inv
  | Co -> Contra
  | Contra -> Co
  | Bi -> Bi
;;

let dot a b =
  match a, b with
  | Inv, Bi ->
      Bi
  | Inv, _ ->
      Inv
  | Co, b ->
      b
  | Contra, b ->
      minus b
  | Bi, _ ->
      Bi
;;

We will now recall our toy language of structural types:

type typ =
  | Sum of typ * typ
  | Prod of typ * typ
  | Unit
  | Var of string
  | App of string * typ list
  | Fun of typ * typ

type defs =
  (string * string list * typ) list

let def_list =
  [ "list", ["a"], Sum (Unit, Prod (Var "a", App ("list", [Var "a"]))) ]

The compute_variance function

let rec compute_variance
    (valuation: string -> variance)
    (t: typ)
    (var_for_ith_param: string -> int -> string)
    (v: string): variance
  =
  match t with
  | Prod (t1, t2)
  | Sum (t1, t2) ->
      let v1 = compute_variance valuation t1 var_for_ith_param v in
      let v2 = compute_variance valuation t2 var_for_ith_param v in
      join v1 v2

  | Unit ->
      Bi

  | Var v' ->
      if v' = v then Co else Bi

  | App (t0, ts) ->
      let vs = List.mapi (fun i t ->
        let formal = valuation (var_for_ith_param t0 i) in
        let effective = compute_variance valuation t var_for_ith_param v in
        dot formal effective
      ) ts in
      List.fold_left join Bi vs

  | Fun (t1, t2) ->
      let v1 = compute_variance valuation t1 var_for_ith_param v in
      let v2 = compute_variance valuation t2 var_for_ith_param v in
      join (minus v1) v2

In the context of Fix, we call variables the unknowns in the system of equations whose value we wish to compute. In the last example, the variables are va, vb, vc and vd. When writing the definition of list a, we will say that a is a parameter for the type list.

In our toy example, Fix variables are of type string.

When computing the variance of a variable in a given type, we need to access the value of the other variables. In the last example, the equation for vc mentions va and vb, meaning we will need both values when evaluating the right-hand side of the vc = equation. This is the purpose of the valuation function.

Another auxiliary function that compute_variance needs is var_for_ith_param, which returns the variable associated to the i-th parameter of another type. For instance, var_for_ith_param t 1 would return vb in the last example.

The definition of this function is straightforward; the only difficult case is App. We use List.mapi as we treat the general case of n-ary type applications; we just need to perform a "join" of all computed variances for all type parameters.

Setting up Fix

Fix uses a functorized interface, the documentation of which is available online. Fix requires imperative maps over its variables; our toy example defines imperative String maps using a reference on a Map.Make(String).t; this is boring so I won't include it here.

Fix also requires the user to define a module that has type PROPERTY. In the Fix jargon, properties are the values for the variables that we wish to solve. In our particular example, a property is a variance. The definition of the module is straightforward.

module P = struct
  type property = variance
  let bottom = Bi
  let equal = (=)
  let is_maximal = (=) Inv
end

Setting up Fix is done through a double-functor application:

module Solver = Fix.Make(IStringMap)(P)

How do we define a system of equations for Fix? A system of equations is a function that maps a variable (e.g. va) to a corresponding property (variance), which is obtained by calling compute_variance on the corresponding right-hand-side. However, computing a property requires, as we mentioned earlier, accessing the values for the other variables: computing va requires knowing the values for vb, vc, vd, as well as the "current" value of va. Computing a right-hand side therefore requires having a valuation for the other variables.

type rhs = valuation -> property

Thus, a system of equations maps variables to right-hand sides.

type equations = variable -> rhs

Naturally, a valuation maps a variable (e.g. va) to a property (e.g. co).

type valuation = variable -> property

Let us now write the equations function:

let solve (defs: defs) =
  (* Build the list of equations. *)
  let equations = fun (var: string) ->
    let _, _, t = 
      (* Find the type definition this variable belongs to. *)
      List.find (fun (_, params, _) ->
        List.exists ((=) var) params
      ) defs
    in
    fun valuation ->
      compute_variance valuation t (var_for_ith_param defs) var
  in

  (* Solve them. *)
  let valuation = Solver.lfp equations in

  valuation

The equations function maps a variable var to a right-hand side. This requires finding, in our list of mutually recursive definitions, the type which this variable belongs to (that is, mapping va to t), and extracting the definition of the type (that is, extracting the definition of t). We then return a function that takes a valuation and computes the variance of the variable in its definition (that is, the value of va under a valuation).

The final call to solve the system is done through Solver.lfp, which just takes the equations function. The amazing part is that we never needed to add the set of variables into the map: this is all done under-the-hood by Fix!

Play with it

The source code is available here.