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.