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.
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
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"]))) ]
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
vd. When writing the definition of
list a, we will say that
a is a parameter for the type
In our toy example,
Fix variables are of type
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
vb, meaning we will need both values when evaluating the right-hand side of the
vc = equation. This is the purpose of the
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.
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
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
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.
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
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
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
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
Play with it
The source code is available here.