## Tuesday, March 21, 2017

### Polynomials over rings

Polynomials over rings

This post provides a workout in generic programming using modules & functors.

The program presented here models univariate polynomials over rings based on an exercise in "The Module Language" chapter, of Didier Rémy's book, Using, Understanding and Unraveling the OCaml Lanaguage.

### Arithmetics and rings

We begin with a type for modules implementing arithmetic.

    module type ARITH = sig
type t
val of_int : int -> t            val to_int : t -> int
val of_string : string -> t      val to_string : t -> string
val zero : t                     val one : t
val add : t -> t -> t            val sub : t -> t -> t
val mul : t -> t -> t            val div : t -> t -> t
val compare : t -> t -> int      val equal : t -> t -> bool
end;;

A ring is a set equipped with two binary operations that generalize the arithmetic operations of addition and multiplication.
    module type RING = sig
type t
type extern_t
val print : t -> unit
val make : extern_t -> t         val show : t -> extern_t
val zero : t                     val one : t
val add : t -> t -> t            val mul : t -> t -> t
val equal : t -> t -> bool
end;;

We can build rings over arithmetics with functors. This particular one fixes the external representation of the elements of the ring to int.
    module Ring (A : ARITH) :
RING  with type t = A.t and type extern_t = int =
struct
include A
type extern_t = int
let make = of_int                let show = to_int
let print x = print_int (show x)
end;;

Thus, here for example are rings over various specific arithmetic modules.
    module Ring_int32 = Ring (Int32);;
module Ring_int64 = Ring (Int64);;
module Ring_nativeint = Ring (Nativeint);;
module Ring_int = Ring (
struct
type t = int
let of_int x = x                   let to_int x = x
let of_string = int_of_string      let to_string = string_of_int
let zero = 0                       let one = 1
let add = ( + )                    let sub = ( - )
let mul = ( * )                    let div = ( / )
let compare = Pervasives.compare   let equal = ( = )
end
);;


### Polynomials

We define now the type of polynomials.

    module type POLYNOMIAL = sig
type coeff (*Type of coefficients*)
type coeff_extern_t (*Type of coeff. external rep*)

(*Polynomials satisfy the ring interface*)
include RING (*Declares a type [t] and [extern_t]*)

(*Function to evaluate a polynomial at a point*)
val eval : t -> coeff -> coeff
end;;

Given a module implementing a ring, we can generate a module implementing polynomials with coefficients drawn from the ring.
    module Polynomial (R : RING) :
POLYNOMIAL with type coeff = R.t
and type coeff_extern_t = R.extern_t
and type extern_t = (R.extern_t * int) list =
struct

type coeff = R.t (*Coefficient type*)
type coeff_extern_t = R.extern_t (*External coeff. rep*)
type extern_t = (coeff_extern_t * int) list (*External polynomial rep*)

(*List of coefficients and their powers*)
type t = (coeff * int) list (*Invariant : Ordered by powers,
lower order terms at the front*)

(* ... *)

end;;

As the comments indicate, the polynomial data structure is a list of pairs of coefficients and powers, ordered so that lower powers come before higher ones. Here's a simple printing utility to aid visualization.
    let print p =
List.iter
(fun (c, k) -> Printf.printf "+ (";
R.print c;
Printf.printf ")X^%d " k)
p

In order that we get a canonical representation, null coefficients are eliminated. In particular, the null monomial is simply the empty list.
    let zero = []

The multiplicative identity one is not really necessary as it is just a particular monomial however, its presence makes polynomials themselves satisfy the interface of rings.
    let one = [R.one, 0]

This helper function constructs monomials.
    let monomial (a : coeff) (k : int) =
if k < 0 then
failwith "monomial : negative powers not supported"
else if R.equal a R.zero then [] else [a, k]

Next up, we define addition of polynomials by the following function. Care is taken to ensure the representation invariant is respected.
    let rec add u v =
match u, v with
| [], _ -> v
| _, [] -> u
| ((c1, k1) :: r1 as p1), ((c2, k2) :: r2 as p2) ->
if k1 < k2 then
(c1, k1) :: (add r1 p2)
else if k1 = k2 then
let c = R.add c1 c2 in
if R.equal c R.zero then add r1 r2
else (c, k1) :: (add r1 r2)
else (c2, k2) :: (add p1 r2)

With monomial and add avaialable, we can now write make that computes a polynomial from an external representation. We also give the inverse function show here too.
    let make l =
List.fold_left (fun acc (c, k) ->
add (monomial (R.make c) k) acc) zero l

let show p =
List.fold_right (fun (c, k) acc -> (R.show c, k) :: acc) p []

The module private function times left-multiplies a polynomial by a monomial.
    let rec times (c, k) = function
| [] -> []
| (c1, k1) :: q ->
let c2 = R.mul c c1 in
if R.equal c2 R.zero then times (c, k) q
else (c2, k + k1) :: times (c, k) q

Given the existence of times, polynomial multiplication can be expressed in a "one-liner".
    let mul p = List.fold_left (fun r m -> add r (times m p)) zero

Comparing two polynomials for equality is achieved with the following predicate.
    let rec equal p1 p2 =
match p1, p2 with
| [], [] -> true
| (c1, k1) :: q1, (c2, k2) :: q2 ->
k1 = k2 && R.equal c1 c2 && equal q1 q2
| _ -> false

In the course of evaluating polynomials for a specific value of their indeterminate, we'll require a function for computing powers. The following routine uses the exponentiation by squaring technique.
    let rec pow c = function
| 0 -> R.one
| 1 -> c
| k ->
let l = pow c (k lsr 1) in
let l2 = R.mul l l in
if k land 1 = 0 then l2 else R.mul c l2

Finally, the function eval for evaluation of a polynomial at a specific point. The implementation uses Horner's rule for computationally efficient evaluation.
    let eval p c = match List.rev p with
| [] -> R.zero
| (h :: t) ->
let reduce (a, k) (b, l) =
let n = pow c (k - l) in
let t = R.add (R.mul a n) b in
(t, l)  in
let a, k = List.fold_left reduce h t in
R.mul (pow c k) a


### Testing and example usage

The following interactive session creates a polynomial with integer coefficients module and uses it to confirm the equivalence of $(1 + x)(1 - x)$ with $(1 - x^{2})$.

    # #use "polynomial.ml";;
# module R = Ring_int;;
# module P = Polynomial (R);;
# let p = P.mul (P.make [(1, 0); (1, 1)]) (P.make [(1, 0); (-1, 1)]);;
# let q = P.make [(1, 0); (-1, 2)];;
# P.equal p q;;
- : bool = true

Polynomials in two variables, can be treated as univariate polynomials with polynomial coefficients. For example, the polynomial $(X + Y)$ can be regarded as $(1 \times X^{1})Y^{0} + (1 \times X^{0})Y^{1}$. Similarly we can write $X - Y$ as $(1 \times X^{1})Y^{0} + (-1 \times X^{0}) Y^1$ and now check the equivalence $(X + Y)(X - Y) = (X^{2} - Y^{2})$.

    #module Y = Polynomial (P);;

#(* (X + Y) *)
#let r = Y.make [
#  ([1, 1], 0); (*(1 X^1) Y^0*)
#  ([1, 0], 1)  (*(1 X^0) Y^1*)
#];;

#(* (X - Y) *)
#let s = Y.make [
#  ([1, 1], 0); (*(1 X^1) Y^0*)
#  ([-1, 0], 1) (*((-1) X^0) Y^1*)
#];;

#(* (X^2 - Y^2) *)
#let t = Y.make [
#  ([1, 2], 0);   (*(1 X^2) Y^0*)
#  ([-1, 0], 2)  (* (-1 X^0) Y^2*)
#];;

#Y.equal (Y.mul r s) t;;
- : bool = true


## Universal type

A universal type is a type into which all other types can be embedded. A module implementing such a type here will satisfy the following signature.

module type UNIVERSAL = sig
type t
val embed : unit → (α → t) * (t → α option)
end;;

The type t is the universal type and each call to embed returns a pair of functions : an injection function for embedding a value into the universal type and, a projection function for extracting the value from its embedding in the universal type. The following code demonstrates intended usage.
module type TEST = sig
val run : unit → unit
end;;

module type UNIVERSAL_TEST = functor (U : UNIVERSAL) → TEST;;

module Basic_usage : UNIVERSAL_TEST =
functor (U : UNIVERSAL) → struct
let run () =
let ((of_int : int → U.t)
, (to_int : U.t → int option)) = U.embed () in
let ((of_string : string → U.t)
, (to_string : U.t → string option)) = U.embed () in

let r : U.t ref = ref (of_int 13) in

begin
assert (to_int !r = Some 13);
assert (to_string !r = None);

r := of_string "foo";

assert (to_string !r = Some "foo");
assert (to_int !r = None);
end
end;;


One possible implementation is via the use of exceptions together with local modules. The core idea exploits the fact that the primitive type exn is an open extensible sum. Here's the complete implementation. We'll break it down later.

module Universal_exn : UNIVERSAL = struct

type t = exn

module type ANY = sig
type c
exception E of c
end

type α any = (module ANY with type c = α)

let mk : unit → α any =
fun (type s) () →
(module struct
type c = s
exception E of c
end : ANY with type c = s)

let inj (type s) (p : s any) (x : s) : t =
let module Any = (val p : ANY with type c = s) in
Any.E x

let proj (type s) (p : s any) (y : t) : s option =
let module Any = (val p : ANY with type c = s) in
match y with
| Any.E x → Some x
| _ as e →  None

let embed () = let p = mk () in inj p, proj p

end;;

Before delving into an explanation of the program, one can verify it satisfies the basic test.
# module Test_basic = Mk_universal_test(Universal_exn);;
# Test_basic.run ();;
- : unit = ()


The definition of the universal type t is an alias to the predefined type exn.

type t = exn

A module type ANY is introduced. Modules that implement this signature define an abstract type c and introduce an exn constructor E of c.
module type ANY = sig
type c
exception E of c
end

An alias for the type of a module value satisfying this signature comes next. Using aliases of this kind are helpful in reducing "syntactic verbosity" in code accepting and returning module values.
type α any = (module ANY with type c = α)

Next follow a set of functions that are private to the implementation of the module. The first of these is mk.
let mk : unit → α any =
fun (type s) () →
(module struct
type c = s
exception E of c
end : ANY with type c = s)

This function mk takes the unit argument and each invocation computes a new module instance which is packed as a first class value and returned. The locally abstract type s connects to the α in the return type.

The next function to be defined is inj which computes a universal type value from its argument.

let inj (type s) (p : s any) (x : s) : t =
let module Any = (val p : ANY with type c = s) in
Any.E x

As was the case for mk, a locally abstract type is used in the definition of inj and observe how that type ensures a coherence between the module parameter p and the type of the parameter to be embedded x.

The projection function proj comes next and also uses a locally abstract type ensuring coherence among its parameters.

let proj (type s) (p : s any) (y : t) : s option =
let module Any = (val p : ANY with type c = s) in
match y with
| Any.E x → Some x
| _ as e →  None

The body of proj unpacks the module value parameter into a module named Any and then attempts to match y against the constructor defined by Any. Recall, at the end of the day, y is of type exn. The match contains two cases : the first matching the constructor Any.E x with x having type s, the second anything else (that is, proj is total).

Finally we come to the public function embed.

let embed () = let p = mk () in inj p, proj p

embed calls mk to produce a new embedding p and returns the pair of partial applications (inj p, proj p).

Our examination of the implementation is concluded. There are however various implications of the implementation we are now in a position to understand that are not immediately obvious from the specification. As a first example, consider the inferred type of a call to embed.

# module U = Universal_exn;;
# let inj, proj = U.embed ();;
val inj : '_a → U.t =
val proj : U.t → '_a option =

Property 1 : embed produces weakly polymorphic functions.

Consider the following scenario:
# let of_int, to_int = U.embed ();;
# let of_string, to_string = U.embed ();;

At this point all of of_int, to_int, of_string and to_string are weakly polymorphic.
# let r : U.t ref = ref (of_int 13);;

The call to of_int fixes it's type to int → U.t and that of to_int to U.t → int option. The types of of_string and to_string remain unfixed.
# to_string !r = Some 13;;
- : bool = false

The programmer has mistakenly used a projection function from a different embedding.
# r := of_string "foo";;
Error: This expression has type string but an expression was expected of
type int

The erroneous usage of to_string incidentally fixed the type of of_string to int → U.t! One can imagine errors of this kind being difficult to diagnose.

Property 2 : Injection/projection functions of different embeddings may not be mixed.

# let ((of_int : int → U.t), (to_int : U.t → int option)) = U.embed ();;
# let ((of_int' : int → U.t), (to_int' : U.t → int option)) = U.embed ();;

Two embeddings have been created, the programmer has fixed the types of the injection/projection functions a priori (presumably as a defense against the problems of the preceding example).
# let r : U.t ref = ref (of_int 13);;
# to_int !r = Some 13;;
- : bool = true

The first embedding is used to inject an integer. That integer can be extracted using the projection function of that embedding.
#  to_int' !r = Some 13;;
- : bool = false

We cannot extract the integer from the universal type value using the projection function from the other embedding despite all of the types involved being the same. One can imagine that also as being quite the source of bugs and confusion to the unknowing programmer.

The constraint of property 2 is beyond the ability of the type system to enforce. About the best one can do is to enhance the specification of the type with documentation.

module type UNIV = sig
type t

val embed : unit → (α → t) * (t → α option)

(* A pair [(inj, proj)] returned by [embed] works together in that
[proj u] will return [Some v] if and only if [u] was created by
[inj v]. If [u] was created by a different function then [proj u]
will return [None]. *)

end;;


## Tuesday, March 7, 2017

### Polymorphic variants : Subtyping and variance

Polymorphic variants : subtyping and variance

## Polymorphic variants : Subtyping and variance

Here are some expressions in the top-level involving polymorphic variant types.

    # let x = [ On; Off ];;
val x : [> Off | On ] list = [ On; Off ]

The notation [> Off | On ] represents a type that at least contains the constructors Off and On. Of course, there are an unlimited number of such types so [> Off | On ] is a set in fact.

    # let n = Number 1;;
val n : [> Number of int ] = Number 1

The value n is of a type that at least contains the constructor Number of int.

    # let f = function | On → 1 | Off → 0 | Number n → n;;
val f : [< Number of int | Off | On ] → int = <fun>

The function f accomodates exactly three cases corresponding to the constructors Off, On and Number of int. This informs us that [< Number of int | Off | On ] is of a type that at most has the constructors Off, On and Number of int.

The expression ($expr$ :> $typexpr$) coerces the expression $expr$ to type $typexpr$. The expression ($expr$ : $typ_{1}$ :> $typ_{2}$ ) coerces the exprssion $expr$ from $typ_{1}$ to $typ_{2}$. It is only possible to coerce an expression $expr$ from type $typ_{1}$ to type $typ_{2}$, if the type of $expr$ is an instance of $typ_{1}$ and $typ_{1}$ is a subtype of $typ_{2}$.

    # let f x = (x :> [ A | B ]);;
val f : [< A | B ] → [ A | B ] = <fun>

We see x needs to be coercible to type [ A | B ]. So, we read [< A | B ] as a type that at most contains the constructors A and B. [ A ], [ B ] and [ A | B ] are the subtypes of [ A | B ]. It follows then that [< A | B ] is the set of subtypes of [ A | B ].

    # let f x = (x :> [ A | B ] * [ C | D ]);;
val f : [< A | B ] * [< C | D ] → [ A | B ] * [ C | D ] = <fun>

We see x needs to be coercible to [ A | B ] * [ C | D ]. This coercion can only proceed if x designates a pair with first component a subtype of [ A | B ] and second component a subtype of [ C | D ]. So we see, [< A | B ] * [< C | D ] is the set of subtypes of [ A | B ] * [ C | D ].

    # let f x = (x  :> [ A ] → [ C | D ]);;
val f : ([> A ] → [< C | D ]) → [ A ] → [ C | D ] = <fun>

We see x needs to be coercible to [ A ] → [ C | D ]. This coercion can only proceed if x designates an arrow where the argument is of a type that at least contains the constructor A. That is [ A ], [ A | ... ] where the "..." represent more constructors. From this we see that [> A] is the set of supertypes of [ A ]. The return value of x (by logic we've already established) is a subtype of [ C | D ]. So, [> A ] → [< C | D ] is the set of subtypes of [ A ] → [ C | D ].

The transformation represented by f above, has coerced an arrow x to a new arrow. The type of the argument of x is [> A ] and the type of the argument of the resulting arrow is [ A ]. That is, for the argument, the transformation between types has taken a supertype to a subtype. The argument type is said to be in a "contravariant" position. On the other hand, the result type of x is [< C | D ] and the arrow that is produced from it, f x, has result type [ C | D ]. That is, the coercion for the result type has taken a subtype to a supertype : the result type in x is said to be in "covariant" position.

In the following, the type α t is abstract.

    # type α t;;
# let f (x : [ A ] t) = (x :> [ A | B ] t);;
Error: Type [ A ] t is not a subtype of [ A | B ] t

Indeed, [ A ] is a subtype of [ A | B ] but that, a priori, does not say anything about the subtyping relationship between [ A ] t and [ A | B ] t. For this coercion to be legal, the parameter α must be given a covariant annotation:
    # type +α t;;
# let f (x : [ A ] t) = (x :> [ A | B ] t);;
val f : [ A ] t → [ A | B ] t = <fun>

The declaration type +α t declares that the abstract type is covariant in its parameter : if the type $\tau$ is a subtype of $\sigma$, then $\tau\;t$ is a subtype of $\sigma\;t$. Here, $\tau =$[ A ], $\sigma =$[ A | B ], $\tau$ is a subtype of $\sigma$ and [ A ] t is a subtype of [ A | B] t.

Here is a similar example, but this time, in the other direction.

    # type α t;;
# let f (x : [ A | B ] t) = (x :> [ A ] t);;
Error: This expression cannot be coerced to type [ A ] t

The type variable can be annotated as contravariant however, and the coercion function typechecks.
    # type -α t;;
# let f (x : [A | B] t) = (x :> [ A ] t);;
val f : [ A | B ] t → [ A ] t = <fun>

The declaration type -α t declares that the abstract type t is contravariant in its parameter : if $\tau$ is a subtype of $\sigma$ then $\sigma\;t$ is a subtype of $\tau\;t$. In this example, $\tau =$[ A ] and $\sigma =$[A | B], $\tau$ is a subtype of $\sigma$ and [ A | B ] t is a subtype of [ A ] t.

In the following, type α t is not abstract and variance can be inferred.

    # type α t = {x : α} ;;
# let f x = (x : [A] t :> [A | B] t);;
val f : [ A ] t → [ A | B ] t = <fun>

Introducing a constraint however inhibits variance inference.
    # type α t = {x : α} constraint α = [< A | B ];;
# let f x = (x : [ A ] t :> [ A | B ] t);;
Error: Type [ A ] t is not a subtype of [ A | B ] t

This situation can be overcome by introducing a covariance annotation.
    # type +α t = {x : α} constraint α = [< A | B ];;
# let f x = (x : [ A ] t :> [ A | B ] t);;
val f : [ A ] t → [ A | B ] t = <fun>

In the following example, α does not participate in the definition of type α t.
    # type α t = {x : int};;
# let f x = (x : [ A ] t :> [ B ] t);;
val f : [ A ] t → [ B ] t = <fun>

In this case, any conversion between δ t and ε t is legal : the types δ and ε are not required to have a subtyping relation between them.

## Saturday, October 29, 2016

### Implementing type-classes as OCaml modules

Implementing type-classes as OCaml modules

## 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.

## Wednesday, October 26, 2016

### Haskell type-classes in OCaml and C++

Haskell type-classes in OCaml and C++

This article examines the emulation of Haskell like type-classes in OCaml and C++. It follows [1] closely (recommended for further reading), extending on some of the example code given there to include C++.

First stop, a simplified version of the Show type-class with a couple of simple instances.

    class Show a where
show :: a -> string

instance Show Int where
show x = Prelude.show x -- internal

instance Show Bool where
str True = "True"
str False = "False"

The OCaml equivalent shown here uses the "dictionary passing" technique for implementation. The type-class declaration Show in Haskell translates to a data-type declaration for a polymorphic record α show in OCaml.
    type α show = {
show : α → string
}

let show_bool : bool show = {
show = function | true → "True" | false → "False"
}

let show_int : int show = {
show = string_of_int
}

In C++ we can use a template class to represent the type-class and specializations to represent the instances.
      template <class A> struct Show {};

template <>
struct Show<int> {
static std::string (*show)(int);
};
std::string(*Show<int>::show)(int) = &std::to_string;

template <>
struct Show<bool> {
static std::string show (bool);
};
std::string Show<bool>::show (bool b) { return b ? "true" : "false"; }


Next up print, a parametrically polymorphic function.

      print :: Show a => a -> IO ()
print x = putStrLn$show x  According to our dictionary passing scheme in OCaml, this renders as the following.  let print : α show → α → unit = fun {show} → fun x → print_endline@@ show x  The key point to note here is that in OCaml, evidence of the α value's membership in the Show class must be produced explicitly by the programmer. In C++, like Haskell, no evidence of the argument's membership is required, the compiler keeps track of that implicitly.  template <class A> void print (A const& a) { std::cout << Show<A>::show (a) << std::endl; }  This next simplified type-class shows a different pattern of overloading : the function fromInt is overloaded on the result type and the (+) function is binary.  class Num a where fromInt :: Int -> a (+) :: a -> a -> a sum :: Num a => [a] -> a sum ls = foldr (+) (fromInt 0) ls  Translation into OCaml is as in the following.  type α num = { from_int : int → α; add : α → α → α; } let sum : α num → α list → α = fun {from_int; add= ( + )} → fun ls → List.fold_right ( + ) ls (from_int 0)  Translation into C++, reasonably mechanical. One slight disappointment is that it doesn't seem possible to get the operator '+' syntax as observed in both the Haskell and OCaml versions.  template <class A> struct Num {}; namespace detail { template <class F, class A, class ItT> A fold_right (F f, A z, ItT begin, ItT end) { if (begin == end) return z; return f (fold_right (f, z, std::next (begin), end), *begin); } }//namespace<detail> template <class ItT> typename std::iterator_traits<ItT>::value_type sum (ItT begin, ItT end) { using A = typename std::iterator_traits<ItT>::value_type; auto add = Num<A>::add; auto from_int = Num<A>::from_int; return detail::fold_right (add, from_int (0), begin, end); }  In Haskell, Int is made a member of Num with this declaration.  instance Num Int where fromInt x = x (+) = (Prelude.+)  Returning to OCaml, we can define a couple of instances including the one above like this.  let int_num : int num = { from_int = (fun x → x); add = Pervasives.( + ); } let bool_num : bool num = { from_int = (function | 0 → false | _ → true); add = function | true → fun _ → true | false → fun x → x }  The code defining those above instances in C++ follows.  template <> struct Num<int> { static int from_int (int); static int add (int, int); }; int Num<int>::from_int (int i) { return i; } int Num<int>::add (int x, int y) { return x + y; } template <> struct Num<bool> { static bool from_int (int); static bool add (bool, bool); }; bool Num<bool>::from_int (int i) { return i != 0; } bool Num<bool>::add (bool x, bool y) { if (x) return true; return y; }  Here now is a function with two type-class constraints.  print_incr :: (Show a, Num a) => a -> IO () print_incr x = print$ x + fromInt 1

In OCaml this can be written like so.
    let print_incr : (α show * α num) → α → unit =
fun (show, {from_int; add= ( + )}) →
fun x → print show (x + (from_int 1))

In C++, this is said as you see below.
    template <class A>
void print_incr (A x) {
print (Num<A>::add (x, Num<A>::from_int (1)));
}

Naturally, the above function will only be defined for types A that are members of both the Show and Num classes and will yield compile errors for types that are not.

Moving on, we now look at another common pattern, an instance with a constraint : a Show instance for all list types [a] when the element instance is a member of Show.

    instance Show a => Show [a] where
show xs = "[" ++ go True xs
where
go _ [] = "]"
go first (h:t) =
(if first then "" else ", ") ++ show h ++ go False t


In OCaml, this takes the form of a function. The idea is, given evidence of a type α's membership in Show the function produces evidence that the type α list is also in Show.
    let show_list : α show → α list show =
fun {show} →
{show = fun xs →
let rec go first = function
| [] → "]"
| h :: t →
(if (first) then "" else ", ") ^ show h ^ go false t in
"[" ^ go true xs
}

It might be possible to do better than the following partial specialization over vector<> in C++ (that is, to write something generic, just once, that works for a wider set ofsequence types) using some advanced meta-programming "hackery", I don't really know. I suspect finding out might be a bit of a rabbit hole best avoided for now.
    template <class A>
struct Show<std::vector<A>> {
static std::string show (std::vector<A> const& ls);
};

template <class A>
std::string Show<std::vector<A>>::show (std::vector<A> const& ls) {
bool first=true;
typename std::vector<A>::const_iterator begin=ls.begin (), end=ls.end ();
std::string s="[";
while (begin != end) {
if (first) first = false;
else s += ", ";
//A compile time error will result here if if there is no
//evidence that A is in Show
s += Show<A>::show (*begin++);
}
s += "]";

return s;
}


In this next example, we need a type-class describing types that can be compared for equality, Eq. That property and the Num class can be combined to produce a type-class with a super-class and a default.

    class Eq where
(==) :: a -> a -> bool
(/=) :: a -> a -> bool

deriving instance Eq Bool
deriving instance Eq Int

class (Eq a, Num a) => Mul a where
(*) :: a -> a -> a
x * _ | x == fromInt 0 = fromInt 0
x * y | x == fromInt 1 = y
x * y | y + (x + (fromInt (-1))) * y

dot :: Mul a => [a] -> [a] -> a
dot xs ys = sum$zipWith ( * ) xs ys  Modeling the above in OCaml is done with a dictionary for the Mul type-class and a function to generate instances from super-class instances.  type α mul = { mul_super : α eq * α num; mul : α → α → α } let mul_default : α eq * α num → α mul = fun (({eq}, {from_int; add = ( + )}) as super) → { mul_super = super; mul = 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 } let bool_mul : bool mul = mul_default (bool_eq, bool_num) let int_mul : int mul = { mul_super = (int_eq, int_num); mul = Pervasives.( * ) } let dot : α mul → α list → α list → α = fun {mul_super = (eq, num); mul} → fun xs ys → sum num@@ List.map2 mul xs ys  As one would expect, expressing the base class/derived class relationships in C++ is playing to its strengths.  template <class A> struct Eq {}; template <> struct Eq<bool> { static bool eq (bool, bool); static bool neq (bool, bool); }; bool Eq<bool>::eq (bool s, bool t) { return s == t; } bool Eq<bool>::neq (bool s, bool t) { return s != t; } template <> struct Eq<int> { static int eq (int, int); static int neq (int, int); }; int Eq<int>::eq (int s, int t) { return s == t; } int Eq<int>::neq (int s, int t) { return s != t; } template <class A> struct Mul : Eq<A>, Num <A> { using Eq<A>::eq; using Num<A>::add; using Num<A>::from_int; static A mul (A x, A y); }; template <class A> A Mul<A>::mul (A x, A y) { if (eq (x, from_int (0))) return from_int (0); if (eq (x, from_int (1))) return y; return add (y, mul ((add (x, from_int (-1))), y)); } template struct Mul<bool>; template <> int Mul<int>::mul (int x, int y) { return x * y; } namespace detail{ template <class F, class It, class Acc> Acc map2 (F f , It xs_begin, It xs_end, It ys_begin, It ys_end, Acc acc) { if ((xs_begin == xs_end) || (ys_begin == ys_end)) return acc; return map2 (f , std::next (xs_begin) , xs_end , std::next (ys_begin) , ys_end , *acc++ = f (*xs_begin, *ys_begin)); } }//namespace detail template <class A> A dot (std::vector<A> const& xs, std::vector<A> const& ys) { std::vector<A> buf; detail::map2 ( Mul<A>::mul , xs.begin (), xs.end() , ys.begin (), ys.end () , std::back_inserter(buf)); return sum (buf.begin (), buf.end ()); }  This very last example is in polymorphic recursion. The Haskell reads as follows.  print_nested :: Show a => Int -> a -> IO () print_nested 0 x = print x print_nested n x = print_nested (n - 1) (replicate n x) test_nested = do n <- getLine print_nested (read n) (5::Int)  Those two functions are very interesting! Translating it to OCaml yields the following.  let rec replicate : int → α → α list = fun n x → if n >= 0 then [] else x :: replicate (n - 1) x let rec print_nested : α. α show → int → α → unit = fun show_dict → function | 0 → fun x → print show_dict x | n → fun x → print_nested (show_list show_dict) (n - 1) (replicate n x) let test_nested = let n = read_int () in print_nested show_int n 5  Now if you examine the output of the above if '4' (say) was entered, you'll see something like this:  [[[[5, 5, 5, 5], [5, 5, 5, 5], [5, 5, 5, 5]], [[5, 5, 5, 5], [5, 5, 5, 5], [5, 5, 5, 5]]]]  You can see, looking at this, that the type of the printed list is not determinable at compile-time. It is dependent on a runtime parameter! It follows that the evidence that the type is in the Show class can not be produced statically. It has to be computed dynamically which is what you see there in the application of show_list to the current show_dict in the n <> 0 branch of the print_nested function. Note also the requirement for the universal quantifier in the function signature. It's mandatory. OK, so how about the above code in C++? Well a naive transliteration gives the following.  namespace detail { template<class A, class ItT> ItT replicate (int n, A x, ItT dst) { if (n <= 0) return dst; return replicate ((n - 1), x, *dst++ = x); } }//namespace detail template <class A> void print_nested (int n, A const& x) { if (n == 0) print (x); else { std::vector<A> buf; detail::replicate(n, x, std::back_inserter(buf)); print_nested (n - 1, buf); } } void test_nested () { int n; std::cin >> n; print_nested (n, 5); }  Unfortunately though, this program though exhibits unbounded compile time recursion (compilation doesn't terminate). References: [1] Implementing, and Understanding Type Classes -- Oleg Kiselyov ## Wednesday, October 12, 2016 ### Monty Hall Suppose you're on a game show, and you're given the choice of three doors : Behind one door is a car; behind the others, goats. You pick a door, say No. 1, and the host, who knows what's behind the doors, opens another door, say No.3 which has a goat. He then says to you, "Do you want to pick door No. 2?" Is it to your advantage to switch your choice? What do you think? This problem is known as the "Monty Hall" problem. It's named after the host of the American television game show "Let's make a deal". Paul Erdős, one of the most prolific mathematicians in history remained unconvinced (of the correct answer to the above problem) until he was shown a computer simulation confirming the predicted result. Here's a simulation in OCaml one hopes, may have convinced Paul! module Monty = struct (*[dtr w p n] where [n] is the number of doors, selects which door to remain (closed) given the winning door [w] and the player chosen door [p]*) let rec dtr w p n = if p <> w then w else if p = 0 then n - 1 else 0 (*[gen_game d] generates a game with [d] doors and returns a game with a winning door, a player selected door and a door to keep closed before if the player wants to switch*) let gen_game (d : int) : (int * int * int) = let w = Random.int d and p = Random.int d in (w, p, dtr w p d) let num_wins = ref 0 (*To keep track of scores*) type strategy = Hold | Switch (*The type of strategies*) (*Play a single game*) let play_game (d : int) (s : strategy) : unit = let w, p, r = gen_game d in match s with | Hold → num_wins := !num_wins + if p = w then 1 else 0 | Switch → num_wins := !num_wins + if r = w then 1 else 0 (*Play a set of [n] games*) let play_games (d : int) (n : int) (s : strategy ) : unit = let rec loop (i : int) : unit = if i = n then () else begin play_game d s; loop (i + 1) end in loop 0 end open Monty (*Initialized from the command line*) let version = ref false let num_doors = ref 0 let num_sims = ref 0 let read_args () = let specification = [("-v", Arg.Set version, "Print the version number"); ("-d", Arg.Set_int num_doors, "Number of doors (>= 3)" ); ("-n", Arg.Set_int num_sims, "Number of simulations (>= 1)"); ] in Arg.parse specification (fun s → Printf.printf "Warning : Ignoring unrecognized argument \"%s\"\n" s) "Usage : monty -d <number of doors> -n <number of simulations>" (*[fabs e] computes the absolute value of [e]*) let fabs (e : float) : float = if e < 0. then ~-.e else e (*Driver*) let () = try read_args (); if !version then Printf.printf "1.0.0\n" else let n = !num_sims and d = !num_doors in if d < 3 then raise (Invalid_argument "Number of doors must be >= than 3"); if n < 1 then raise (Invalid_argument "Number of simulations must be >= 1"); begin (*Hold*) num_wins := 0; play_games d n Hold; Printf.printf "Num wins (hold): %d\n" !num_wins; let err=fabs (float_of_int (!num_wins) /. (float_of_int n) -. 1.0 /. (float_of_int d)) in Printf.printf "Error %f\n" err; (*Switch*) num_wins := 0; play_games d n Switch; Printf.printf "Num wins (switch): %d\n" !num_wins; let err=fabs (float_of_int (!num_wins) /. (float_of_int n) -. (float_of_int (d - 1) /. (float_of_int d))) in Printf.printf "Error %f\n" err ; end with | Invalid_argument s → Printf.printf "%s\n" s  ## Wednesday, October 5, 2016 ### Conversion operations of the lambda-calculus Conversion #### Abstract This note provides a super lightweight explanation of the three conversion operations of the$\lambda$-calculus known (cryptically) as$\alpha$,$\beta$and$\eta$conversions respectively (borrowed fairly freely from the delightful reference given at the bottom.) #### Syntax vs. semantics The$\textbf{syntax}$of the language of$\textit{$\lambda$- expressions}$is $\begin{eqnarray} <exp> & ::= & <constant>\;\; & \text{Constants} \nonumber \\ & \mid & <variable>\;\; & \text{Variables} \nonumber \\ & \mid & <exp> <exp>\;\; & \text{Applications} \nonumber \\ & \mid & \lambda<variable>.<exp>\;\; & \text{Abstractions} \nonumber \end{eqnarray}$ The$\textbf{semantics}$of the the$\lambda$-calculus is defined by three$\textit{conversion rules}$. To understand them requires the terminology of$\textit{free}$and$\textit{bound}$variables. An occurence of a variable in a$\lambda$-expression is bound if there is an enclosing abstraction that binds it, and is free otherwise. For example, in$\lambda x.+\; ((\lambda y. +\;y\; z)\;7)\;x$,$x$and$y$appear bound whereas$z$appears free. ####$\beta$-conversion$\beta$-reduction describes how to apply a function to an argument. For example,$\left(\lambda x.+\;x\;1\right)\; 4$denotes the application of a particular$\lambda$-abstraction to the argument$4$. The result of applying a$\lambda$-abstraction to an argument is an instance of the body of the$\lambda$-abstraction in which (free) occurences of the formal parameter in the body are replaced with (copies of) the argument. Thus,$\left(\lambda x.+\;x\;1\right)\; 4 \rightarrow +\;4\;1 \rightarrow 5$. In the event there are no occurences of the formal parameter in the abstraction body, the argument is discarded unused so,$(\lambda x.\;3)\;4 \rightarrow 3$. Care is needed when formal parameter names are not unique. For example, $\begin{eqnarray} & & \left(\lambda x.\;\left(\lambda x.+ \left(-\;x\;1\right)\right)\;x\;3\right)\; 9 \nonumber \\ & \rightarrow & \left(\lambda x.+ \left(-\;x\;1\right)\right)\;9\;3 \nonumber \\ & \rightarrow & +\;\left(-\;9\;1\right)\;3 \nonumber \\ & \rightarrow & +\;8\;3 \nonumber \\ & \rightarrow & 11 \nonumber \end{eqnarray}$ The key point of that example is that we did not substitue for the inner$x$in the first reduction because it was not free in the body of the outer$\lambda x$abstraction. Indeed, in the OCaml top-level we observe  # (fun x -> (fun x -> ( + ) (( - ) x 1)) x 3) 9 ;; - : int = 11  or equivalently, in C++,  auto add = [](int x) { return [=](int y) { return x + y; }; }; auto sub = [](int x) { return [=](int y) { return x - y; }; }; [=](int x) { return [=](int x) { return add (sub (x) (1)); } (x) (3); } (9) ; //is the value '11'  The$\beta$-rule applied backwards is called$\beta$-abstraction and written with a backwards reduction arrow '$\leftarrow$'. Thus,$+\;4\;1 \leftarrow (\lambda x.\;+\;1\;x)\;4$.$\beta$-conversion means reduction or abstraction and is written with a double-ended arrow augmented with a$\beta$(in order to distinguish it from other forms of conversion). So,$+\;4\;1 \underset{\beta}{\leftrightarrow} (\lambda x.\;+\;1\;x)\;4$. One way to look at$\beta$conversion is that it is saying something about$\lambda$-expressions that look different but mean the same thing. ####$\alpha$-conversion It seems obvious that the two abstractions$\lambda x.+\;x\;1$and$\lambda y.+\;y\;1$"ought" to be equivalent.$\alpha$-conversion allows us to change the name of a formal parameter as long as it is done consistently. So we write$\lambda x.+\;x\;1 \underset{\alpha}{\leftrightarrow} \lambda y.+\;y\;1$. Of course, the newly introduced name must not occur free in the body of the original$\lambda$-abstraction. ####$\eta$-conversion This last conversion rule exists to to complete our intuition about what$\lambda$-abstractions "ought" to be equivalent. The rule is this : If$f$denotes a function,$x$a variable that does not occur free in$f$, then$\lambda x.f\;x \underset{\eta}{\leftrightarrow} f$. For example, in OCaml if we define f by let f x = x + 1 then clearly fun x -> f x produces the same results for all values x in the domain of f. #### Summary The first section provides a set of formal rules for constructing expressions (the BNF grammar). Using the notation$E\;\left[M/x\right]$to mean the expression$E$with$M$substituted for free occurrences of$x\$ we can succintly state the the rules for converting one expression into an equivalent one as $\begin{eqnarray} x\;\left[M/x\right] & = & M \nonumber \\ c\;\left[M/x\right] & = & c\;\;\text{where c is any variable or constant other than x} \nonumber \\ \left(E\;F\right)\;\left[M/x\right] & = & E\left[M/x\right]\; F\left[M/x\right]\; \nonumber \\ \left(\lambda x.E\right)\;\left[M/x\right] & = & \lambda x.E \nonumber \\ \left(\lambda y.E\right)\;\left[M/x\right] & & \text{where y is any variable other than x} \nonumber \\ & = & \lambda y.E\left[M/x\right]\;\text{if x does not occur free in E or y does not occur free in M} \nonumber \\ & = & \lambda z.\left(E\left[z/y\right]\right)\left[M/x\right]\;\text{otherwise}\nonumber \\ \end{eqnarray}$

References:
[1] The Implementation of Functional Programming Languages by Simon L. Peyton Jones. 1987.