Modular type classes
We revisit the idea of type-classes first explored in this post. This time though, the implementation technique will be by via OCaml modules inspired by the paper "Modular Type Classes"  by Harper et. al.
Starting with the basics, consider the class of types whose
values can be compared for equality. Call this
Eq. We represent the class as a
module type EQ = sig type t val eq : t * t → bool endSpecific instances of
Eqare modules that implement this signature. Here are two examples.
module Eq_bool : EQ with type t = bool = struct type t = bool let eq (a, b) = a = b end module Eq_int : EQ with type t = int = struct type t = int let eq (a, b) = a = b end
Given instances of class
Y say,) we realize that products of those
instances are also in
Eq. This idea can be
expressed as a functor with the following type.
module type EQ_PROD = functor (X : EQ) (Y : EQ) → EQ with type t = X.t * Y.tThe implementation of this functor is simply stated as the following.
module Eq_prod : EQ_PROD = functor (X : EQ) (Y : EQ) → struct type t = X.t * Y.t let eq ((x1, y1), (x2, y2)) = X.eq (x1, x2) && Y.eq(y1, y2) endWith this functor we can build concrete instances for products. Here's one example.
module Eq_bool_int : EQ with type t = (bool * int) = Eq_prod (Eq_bool) (Eq_int)
Eq can be used as a building
block for the construction of new type classes. For example, we
might define a new type-class
Ord that admits
types that are equality comparable and whose values can be ordered
with a "less-than" relation. We introduce a new module type to
describe this class.
module type ORD = sig include EQ val lt : t * t → bool endHere's an example instance of this class.
module Ord_int : ORD with type t = int = struct include Eq_int let lt (x, y) = Pervasives.( < ) x y endAs before, given two instances of this class, we observe that products of these instances also reside in the class. Accordingly, we have this functor type
module type ORD_PROD = functor (X : ORD) (Y : ORD) → ORD with type t = X.t * Y.twith the following implementation.
module Ord_prod : ORD_PROD = functor (X : ORD) (Y : ORD) → struct include Eq_prod (X) (Y) let lt ((x1, y1), (x2, y2)) = X.lt (x1, x2) || X.eq (x1, x2) && Y.lt (y1, y2) endThis is the corresponding instance for pairs of intgers.
module Ord_int_int = Ord_prod (Ord_int) (Ord_int)Here's a simple usage example.
let test_ord_int_int = let x = (1, 2) and y = (1, 4) in assert ( not (Ord_int_int.eq (x, y)) && Ord_int_int.lt (x, y))
Using type-classes to implement parameteric polymorphism
This section begins with the
module type SHOW = sig type t val show : t → string endIn what follows, it is convenient to make an alias for module values of this type.
type α show_impl = (module SHOW with type t = α)Here are two instances of this class...
module Show_int : SHOW with type t = int = struct type t = int let show = Pervasives.string_of_int end module Show_bool : SHOW with type t = bool = struct type t = bool let show = function | true → "True" | false → "False" end... and here these instances are "packed" as values.
let show_int : int show_impl = (module Show_int : SHOW with type t = int) let show_bool : bool show_impl = (module Show_bool : SHOW with type t = bool)The existence of the
Showclass is all that is required to enable the writing of our first parametrically polymorphic function.
let print : α show_impl → α → unit = fun (type a) (show : a show_impl) (x : a) → let module Show = (val show : SHOW with type t = a) in print_endline@@ Show.show x let test_print_1 : unit = print show_bool true let test_print_2 : unit = print show_int 3The function
αas long as the caller can produce evidence of
α's membership in
Show(in the form of a compatible instance).
The next example begins with the definition of a
Num (the class of additive numbers)
together with some example instances.
module type NUM = sig type t val from_int : int → t val ( + ) : t → t → t end module Num_int : NUM with type t = int = struct type t = int let from_int x = x let ( + ) = Pervasives.( + ) end let num_int = (module Num_int : NUM with type t = int) module Num_bool : NUM with type t = bool = struct type t = bool let from_int = function | 0 → false | _ → true let ( + ) = function | true → fun _ → true | false → fun x → x end let num_bool = (module Num_bool : NUM with type t = bool)The existence of
Numadmits writing a polymorphic function
sumthat will work for any
α listof values if only
αcan be shown to be in
let sum : α num_impl → α list → α = fun (type a) (num : a num_impl) (ls : a list) → let module Num = (val num : NUM with type t = a) in List.fold_right Num.( + ) ls (Num.from_int 0) let test_sum = sum num_int [1; 2; 3; 4]This next function requires evidence of membership in two classes.
let print_incr : (α show_impl * α num_impl) → α → unit = fun (type a) ((show : a show_impl), (num : a num_impl)) (x : a) → let module Num = (val num : NUM with type t = a) in let open Num in print show (x + from_int 1) (*An instantiation*) let print_incr_int (x : int) : unit = print_incr (show_int, num_int) x
α is in
Show then we
can easily extend
Show to include the
α list. As we saw earlier, this kind of
thing can be done with an approriate functor.
module type LIST_SHOW = functor (X : SHOW) → SHOW with type t = X.t list module List_show : LIST_SHOW = functor (X : SHOW) → struct type t = X.t list let show = fun xs → let rec go first = function |  → "]" | h :: t → (if (first) then "" else ", ") ^ X.show h ^ go false t in "[" ^ go true xs endThere is also another way : one can write a function to dynamically compute an
α list show_implfrom an
let show_list : α show_impl → α list show_impl = fun (type a) (show : a show_impl) → let module Show = (val show : SHOW with type t = a) in (module struct type t = a list let show : t → string = fun xs → let rec go first = function |  → "]" | h :: t → (if (first) then "" else ", ") ^ Show.show h ^ go false t in "[" ^ go true xs end : SHOW with type t = a list) let testls : string = let module Show = (val (show_list show_int) : SHOW with type t = int list) in Show.show (1 :: 2 :: 3 :: )
Mul is an aggregation of the
together with a function to perform multiplication.
module type MUL = sig include EQ include NUM with type t := t val mul : t → t → t end type α mul_impl = (module MUL with type t = α) module type MUL_F = functor (E : EQ) (N : NUM with type t = E.t) → MUL with type t = E.tA default instance of
Mulcan be provided given compatible instances of
module Mul_default : MUL_F = functor (E : EQ) (N : NUM with type t = E.t) → struct include (E : EQ with type t = E.t) include (N : NUM with type t := E.t) let mul : t → t → t = let rec loop x y = begin match () with | () when eq (x, (from_int 0)) → from_int 0 | () when eq (x, (from_int 1)) → y | () → y + loop (x + (from_int (-1))) y end in loop end module Mul_bool : MUL with type t = bool = Mul_default (Eq_bool) (Num_bool)Specific instances can be constructed as needs demand.
module Mul_int : MUL with type t = int = struct include (Eq_int : EQ with type t = int) include (Num_int : NUM with type t := int) let mul = Pervasives.( * ) end let dot : α mul_impl → α list → α list → α = fun (type a) (mul : a mul_impl) → fun xs ys → let module M = (val mul : MUL with type t = a) in sum (module M : NUM with type t = a)@@ List.map2 M.mul xs ys let test_dot = dot (module Mul_int : MUL with type t = int) [1; 2; 3] [4; 5; 6]Note that in this definition of
dot, coercision of the provided
Mulinstance to its base
Numinstance is performed.
This last section provides an example of polymorphic recursion
utilizing the dynamic production of evidence by way of
show_list function presented earlier.
let rec replicate : int → α → α list = fun n x → if n <= 0 then  else x :: replicate (n - 1) x let rec print_nested : α. α show_impl → int → α → unit = fun show_mod → function | 0 → fun x → print show_mod x | n → fun x → print_nested (show_list show_mod) (n - 1) (replicate n x) let test_nested = let n = read_int () in print_nested (module Show_int : SHOW with type t = int) n 5