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