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.
Ad hoc polymorphism | |
|
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) |
Listing 1 |
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 |
Listing 2 |
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 :: []) |
Listing 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 |
Listing 4 |
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) |
Listing 5 |
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] |
Listing 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 |
Listing 7 |
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
Overload Journal #142 - December 2017 + Programming Topics
Browse in : |
All
> Journals
> Overload
> o142
(7)
All > Topics > Programming (877) Any of these categories - All of these categories |