# Comparing Monads in Haskell and in OCaml

*25 Feb 2021*

## 1.

In the introduction part of the paper Lightweight Higher-kinded Polymorphism, the authors compared
two implementations of the `when`

function: one in OCaml and the other in Haskell.

The `when`

function as defined in Haskell is not simply a conditional with a
default. More importantly, the types of the branches are monadic.
For instance, the default branch `return ()`

(read "return unit") is a
higher-kinded polymorphic term of type `Monad m => m ()`

(read: "m unit, where
the type constructor m can be any monad", or simply "monad unit"); and `return`

itself has
type `Monad m => a -> m a`

(read: "a arrow m a, where the type constructor m can be any monad, and a can be any type", or simply "a arrow monad a").

In OCaml, the difficulty of implementing `when`

lies not in the conditional
but in the higher-kinded polymorphic `return`

function, for OCaml does not
support type variables of higher-kind: the higher-kinded type variables
(the `m`

's) in the signatures in the above paragraph have no parallel in OCaml.

The authors then point out that OCaml provides *module functors* to abstract
over type constructors, and show a way to implement `when`

in OCaml, subject
to the reader's know-how about implementing monads in OCaml.

I observe that the difference
between monads in OCaml and monads in Haskell is the root of the
difference between the `when`

functions.

## 2.

First let's see the similarity between monads in the two languages: why they are essentially the same so that we can call them both "monads"?

In OCaml, a monad is a module featuring an abstract unary type constructor with
an arbitrary name, say `t`

, and two monadic operators on `t`

which are `return`

and `>>=`

(read: "bind"). What is important about `t`

is not its name, but
its number of type parameters: 1, and the two operators on it: "return"
and "bind". This is exactly what is captured by the `Monad`

constructor class
in Haskell.

Now we compare the difference.

In Haskell, to declare a type constructor
as a monad, we simply need to declare it as an instance of
the `Monad`

class, and provide an implementation of the monadic operators
and perhaps check that the monadic laws hold.

While, in OCaml we begin with defining a module type `Monad`

consisting of
an abstract type constructor and the signatures of the two monadic operators;
the former (i.e., the abstract type constructor) corresponds in spirit to the constructor class parameter in Haskell, and the latter (i.e. the signatures
of the monadic operators) corresponds directly to the operator type
declarations in the Haskell constructor class. For each concrete type
constructor which we want to declare as a monad, we must define a module
in which we alias the type constructor and implement the
monadic operators in such a way that the module can be masked by the
`Monad`

module type.

## 3.

Such difference in monad representation entails that there is
one monadic `return`

function in Haskell which receives the type
`Monad m => a -> m a`

but there are infinitely many monadic
`return`

functions in OCaml each receiving a type where there is no polymorphism on
type constructors. This resembles the
contradiction between Church typing and Curry typing; for instance,
there is only one identity function by Curry typing, which receives a parametric polymorphic type, but there are infinitely many identity functions by Church
typing each receiving a concrete type.

It is because we have infinitely many monadic `return`

functions in OCaml
, each from a module that implements a specific monad, that we
have infinitely many `when`

functions in OCaml, each comes from an application
of the `When`

module functor to a module that implements a specific monad and
provides a specialized `return`

function.

## 4.

The interesting conclusion is that if a Haskell function has a higher-kinded polymorphic type, and we want to implement the function in OCaml, it is inevitable that we end up with a family of type-specific versions of the function defined by means of modules and module functors.

## Follow-up Comments

Below are some follow-up comments on the blog.

### The monadic `return`

is overloaded, or (higher-kinded) parametric polymorphic ?

*03 March 2021; edited on 09 March 2021*

In Section 1 of the blog, I wrote that the monadic `return`

function
is higher-kinded polymorphic. I later noticed that the authors of the
*Lightweight Higher-kinded Polymorphism* paper do not consider `return`

in
Haskell as being (higher-kinded) parametric polymorphic; instead, they
call it overloaded. Here I clarify the concepts.

Overloading and parametric polymorphism are two distinct
concepts: for a parametric polymorphic function its different type-specific
instances share exactly the same function definition, e.g., reversal of
a list is irrelevant to the list member type and the function definition
is the same for lists of characters, strings, integers, booleans or floats
etc.; for an overloaded function its different type-specific instances
definitely have different function definitions, e.g., the definition
of `return`

for a Maybe Monad is a "Maybe" wrapper, while for a List Monad
the definition of `return`

becomes a singleton-list wrapper. In other words,
an overloaded Haskell function and a parametric polymorphic function may have
type signatures that look similar: in both cases there are type variabes
that can be instantiated to obtain signatures of type-specific instances
of the function; however, a parametric polymorphic function has only one
concrete definition or embodiment, but an overloaded function has as many
concrete definitions or embodiments as the types for which the function
is overloaded.

Assigning a type to an overloaded function by means of a constructor class
(such as the `Monad`

class in Haskell) results in occurrences of
type variables in the signatures of certain functions; but occurrence of
instantiable type variables in the type signature does not imply that a
function so typed is necessarily parametric polymorphic.

To be more precise, the monadic `return`

function is a (higher-kinded)
*ad-hoc* polymorphic function (overloading = ad-hoc polymorphism), but
not a *parametric* polymorphic function.
It is therefore correct to say (albeit less precisely) that it is a
higher-kinded polymorphic function (as I say in Section 1).

### The subtlety of checking type equality in OCaml

*09 March 2021*

Following a comparison of the `when`

function in Haskell with that in
OCaml, the authors comment that the extra heaviness of writing `when`

in OCaml
comes directly from the lack of overloading in the language; but more deeply (or more
generally) the reason is the lack of higher-kinded polymorphism.

I understand that `return`

is higher-kinded ad-hoc polymorphic. To have higher-kinded
ad-hoc polymorphism in OCaml, which is a special form of higher-kinded polymorphism,
we must provide what is required by *any* form of higher-kinded polymorphism, be it ad-hoc
or parametric; we must allow type variables of higher-kinds,
or some other way of abstracting over higher-kinded type constructors.

Then the authors move on to discuss the *alias problem*. They begin with the
argument that checking type equality is easier in Haskell than in OCaml. I have some
comments here.

I understand that in Haskell there is no way to hide a type equation (aka. a type synonym); only data constructors can be hidden and the programmer can choose to hide all or only some of the data constructors of an algebraic data type. But in OCaml, a type equation can be hidden; data constructors are exported in an all-or-nothing manner. In the above sense (and compared with Haskell) OCaml offers more flexibility for hiding type equations, but less flexibility for hiding data constructors.

The authors say that an OCaml module signature (aka. module type) *may* temporarily
abstract a type in the case of applying a module functor. This is true and this is indeed
a subtle technical point of OCaml modules. OCaml functors require that their argument
modules must match the module types specified in the functor definitions. Explicit argument
module types in a functor definition tells what the functor assumes about
its argument modules, but these module types as functor argument specifications have no
effect on what the type checker can see about the argument modules. A functor can assume
about an argument module no more than what is given in the argument signature but outside
the functor, the type checker could see the full picture of the argument module which is
given by the module's own signature.

*This blog post is also on GitHub with some extra code examples.*