A toy type language (3) using Fix to compute variance
- January 21, 2014
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.