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