```(* Section 3 *)

let rec list_remove_all e = function
| [] -> []
| e' :: q ->
if e = e' then list_remove_all e q
else e' :: list_remove_all e q

(****************************************************)

type var
type typeconstr

(* Solution using polymorphic variants *)
module VP = struct

type monotype = [ `Var of var | `Constr of typeconstr * monotype list ]

type ('a, 'b) bound = [ `Bound of (var * 'a) * 'b ]
type bot = [ `Bottom ]

type polytype = [ monotype | bot | (polytype, polytype) bound ]

(* Free type variables *)
let rec ftv_monotype : monotype -> _ = function
| `Var v -> [v]
| `Constr (_, l) -> List.concat (List.map ftv_monotype l)
and ftv_polytype : polytype -> _ = function
| #monotype as m -> ftv_monotype m
| `Bottom -> []
| `Bound ((v, t), t') ->
ftv_polytype t @ (list_remove_all v (ftv_polytype t'))

(* Substitution of a variable by a monotype *)
let rec expand_mono_in_mono (v, m) = function
| `Var v' -> if v = v' then m else `Var v'
| `Constr (c, l) -> `Constr (c, List.map (expand_mono_in_mono (v, m)) l)
and expand_mono_in_poly (v, m) : polytype -> _ = function
| #monotype as m' -> (expand_mono_in_mono (v, m) m' :> polytype)
| `Bottom -> `Bottom
| `Bound ((v', t), t') ->
`Bound ((v', expand_mono_in_poly (v, m) t),
if v = v' then t' else expand_mono_in_poly (v, m) t')

(* Types for the normal form *)
type constr = [ `Constr of typeconstr * monotype list ]

type nf_polytype = [ monotype | bot | (bot_poly, constr_poly) bound ]
and bot_poly  =    [            bot | (bot_poly, constr_poly) bound ]
and constr_poly =  [ constr   |       (bot_poly, constr_poly) bound ]

let rec nf : polytype -> nf_polytype = function
| #bot | #monotype as t -> t
| `Bound ((v, t), t') ->
match nf t with
| #monotype as m' -> nf (expand_mono_in_poly (v, m') t') (* Eq-Mono*)
| #bot_poly as t ->
match nf t' with
| `Var v' ->
if v = v' then t (* Eq-Var *)
else `Var v' (* Eq-Free *)
| #bot -> `Bottom (* Eq-Free *)
| #constr_poly as t' ->
let ftv = ftv_polytype (t' : constr_poly :> polytype) in
if List.mem v ftv then `Bound ((v, t), t')
else t' (* Eq-Free *)
end

(* Solution using standard inductive *)
module IND = struct

type monotype = Var of var | Constr of constr
and constr = typeconstr * monotype list

type ('a, 'b) bound = (var * 'a) * 'b

type polytype =
Mono of monotype  | Bot  | Bound of  (polytype, polytype)    bound
type nf_poly =
Mono1 of monotype | Bot1 | Bound1 of (bot_poly, constr_poly) bound
and constr_poly =
Constr3 of constr |        Bound3 of (bot_poly, constr_poly) bound
and bot_poly =          Bot2 | Bound2 of (bot_poly, constr_poly) bound

(* Substitution of variables by monotypes *)
let rec expand_mono_in_mono (v, m) = function
| Var v' -> if v = v' then m else Var v'
| Constr (c, l) -> Constr (c, List.map (expand_mono_in_mono (v, m)) l)

let rec expand_mono_in_poly (v, m) = function
| Mono m' -> Mono (expand_mono_in_mono (v, m) m')
| Bot -> Bot
| Bound ((v', t), t') ->
Bound ((v', expand_mono_in_poly (v, m) t),
if v = v' then t' else expand_mono_in_poly (v, m) t')

(* Free type variables on bounds, monotypes, polytypes dans subsets
of polytypes. We try to reuse as much code as possible *)
let ftv_bound ((v, t), t' : (_, _) bound) f1 f2 =
f1 t @ (list_remove_all v (f2 t'))

let rec ftv_monotype = function
| Var v -> [v]
| Constr (_, l) -> ftv_list_monotype l
and ftv_list_monotype l = List.concat (List.map ftv_monotype l)
(* Not used in the solution
and ftv_polytype = function
| Mono m -> ftv_monotype m
| Bot -> []
| Bound b -> ftv_bound b ftv_polytype ftv_polytype
*)

let rec ftv_poly = function
| Bot2 -> []
| Bound2 b -> ftv_bound' b
and ftv_constr = function
| Constr3 (_, l) -> ftv_list_monotype l
| Bound3 b -> ftv_bound' b
and ftv_bound' b = ftv_bound b ftv_poly ftv_constr

(* Projection of constr_poly and bot_poly into nf_poly. In constant time *)
let bot_to_nf = function
| Bot2 -> Bot1
| Bound2 b -> Bound1 b
let constr_to_nf = function
| Constr3 b -> Mono1 (Constr b)
| Bound3 b -> Bound1 b

let rec nf = function
| Mono m -> Mono1 m
| Bot -> Bot1
| Bound ((v, t), t') ->
let aux1 nft =
let aux2 nft' =
let ftv = ftv_constr nft' in
if List.mem v ftv then Bound1 ((v, nft), nft')
else (constr_to_nf nft')
in
match nf t' with
| Bot1 -> Bot1
| Mono1 (Var v') ->
if v = v' then (bot_to_nf nft)
else (Mono1 (Var v'))
| Mono1 (Constr b) -> aux2 (Constr3 b)
| Bound1 b' -> aux2 (Bound3 b')
in
match nf t with
| Mono1 m -> nf (expand_mono_in_poly (v, m) t')
| Bound1 b -> aux1 (Bound2 b)
| Bot1 -> aux1 Bot2

end
```

This document was generated using caml2html