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" [2] by Harper et. al.
Starting with the basics, consider the class of types whose
values can be compared for equality. Call this
type-class Eq. We represent the class as a
module signature.
module type EQ = sig
type t
val eq : t * t → bool
end
Specific instances of Eq are 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 Eq (X
and 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.t
The 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)
end
With 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)
The class 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
end
Here'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
end
As 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.t
with 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)
end
This 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 Show type-class.
module type SHOW = sig
type t
val show : t → string
end
In 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 Show class 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 3
The function print can be used with values of any
type α 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
type-class 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 Num admits writing a
polymorphic function sum that will work for
any α list of values if only α
can be shown to be in Num.
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
If α is in Show then we
can easily extend Show to include the
type α 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
end
There is also another way : one can write a function to dynamically
compute an α list show_impl from an α
show_impl.
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 :: [])
The type-class Mul is an aggregation of the
type-classes Eq and Num
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.t
A default instance of Mul can be provided given
compatible instances of Eq
and Num.
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 Mul instance to its
base Num instance is performed.
This last section provides an example of polymorphic recursion
utilizing the dynamic production of evidence by way of
the 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
References:
[1] Implementing, and Understanding Type Classes -- Oleg Kiselyov
[2] Modular Type Classes -- Harper et. al.
