Comparing Monads in Haskell and in OCaml

25 Feb 2021


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.


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.


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.


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.