Implementing Type-Classes as OCaml Modules

Modular type classes

In this article, we revisit the idea of type-classes first explored in a previous blog post [ Fletcher16a ]. This time though, the implementation technique will be by via OCaml modules inspired by the paper ‘Modular Type Classes’ [ Dreyer07 ] by Dreyer 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 integers.

  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 parametric 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 'a show_impl = (module SHOW with type t = 'a)

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 : 'a show_impl → 'a → 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 'a as long as the caller can produce evidence of 'a ’s membership in Show (in the form of a compatible instance).

Listing 1 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

type 'a num_impl = (module NUM with type t = 'a)

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 'a list of values if only 'a can be shown to be in Num .

  let sum : 'a num_impl → 'a list → 'a =
    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 : ('a show_impl * 'a num_impl)
      → 'a → 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 'a is in Show then we can easily extend Show to include the type 'a list . As we saw earlier, this kind of thing can be done with an appropriate functor. (See Listing 2.)

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 'a list show_impl from an 'a show_impl (see Listing 3).

let show_list : 'a show_impl → 'a 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. (Listing 4.)

module type MUL = sig
  include EQ
  include NUM with type t := t

  val mul : t → t → t
end

type 'a mul_impl = (module MUL with type t = 'a)

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 . (See Listing 5.)

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 (Listing 6).

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 : 'a mul_impl → 'a list → 'a list → 'a
  = 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 , coercion of the provided Mul instance to its base Num instance is performed.

Listing 7 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 → 'a → 'a list =
  fun n x → if n <= 0 
    then [] else x :: replicate (n - 1) x
let rec print_nested : 'a. 'a show_impl → 
  int → 'a → 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
			

This article was previously published as a blog post in 2016. [ Fletcher16b ] and the source is available at: https://github.com/shayne-fletcher/overload-2017/blob/master/mod.ml

References

[Dreyer07] Derek Dreyer, Robert Harper and Manuel M. T. Chakravarty, ‘Modular Type Classes’, 2007, available online at http://www.cse.unsw.edu.au/~chak/papers/mtc-popl.pdf

[Fletcher16a] Shayne Fletcher, ‘Haskell type-classes in OCaml and C++’, available at http://blog.shaynefletcher.org/2016/10/haskell-type-classes-in-ocaml-and-c.html

[Fletcher16b] Shayne Fletcher, ‘Implementing type-classes as OCaml modules’, available at http://blog.shaynefletcher.org/2016/10/implementing-type-classes-as-ocaml.html

[Kiselyov14] Oleg Kiselyov, ‘Implementing, and Understanding Type Classes’, updated November 2014, available at http://okmij.org/ftp/Computation/typeclass.html