Higher-kinded bounded polymorphism in OCaml (2021)

• Introduction
• Why higher-kinded polymorphism is not supported directly in OCaml
• Higher-kinded functions as Functors
• Yallop and White’s Lightweight higher-kinded polymorphism
• Sidestepping higher-kinded polymorphism
• Algebras
• What’s in a higher-kinded type name
• Conclusions

Introduction

“Polymorphism abstracts types, just as functions abstract
values. Higher-kinded polymorphism takes things a step further,
abstracting both types and types constructors, just as higher-order
functions abstract both first-order values and functions.” — write
Yallop and White (FLOPS 2014).

This remarkably concise summary is worth expounding upon, to
demonstrate how (bounded) higher-kinded polymorphism tends to
arise. The example introduced here is used all throughout the page.

Summing up numbers frequently occurs in practice; abstracting from
concrete numbers leads to a function — an operation that can be
uniformly performed on any collection (list) of numbers:

    let rec sumi : int list -> int = function [] -> 0 | h::t -> h + sumi t

We may further abstract over 0 and the operation
+, which itself is a function (a parameterized value, so to
speak). The result is a higher-order function:

    let rec foldi (f: int->int->int) (z: int) : int list -> int =
        function [] -> z | h::t -> f h (foldi f z t)

Folding over a list, say, of floating-point numbers proceeds similarly, so we
may abstract yet again — this time not over values but over the type
int, replacing it with a type variable:

    let rec fold (f: 'a->'a->'a) (z: 'a) : 'a list -> 'a =
        function [] -> z | h::t -> f h (fold f z t)

thus giving us the polymorphic function: the function that describes an
operation performed over lists of various types, uniformly.
The operation f and the value z can be collected into a
parameterized record

    type 'a monoid = {op: 'a->'a->'a; unit: 'a}

The earlier fold then takes the form

    let rec foldm (m: 'a monoid) : 'a list -> 'a =
        function [] -> m.unit | h::t -> m.op h (foldm m t)

When using foldm on a concrete list of the type t list,
the type variable 'a gets
instantiated to the type t of the elements of this list. The type is not
completely arbitrary, however: there must exist the value
t monoid, to be passed to foldm as the argument. We say the type
t must (at least) implement/support the 'a monoid interface; the t monoid value is then the witness that t indeed does so. Hence the
polymorphism in foldm is bounded.

Exercise: if 'a monoid really describes a monoid,
op x unit = x holds. Write a more optimal version of foldm (and
its subsequent variants) taking advantage of this identity.

A file, a string, an array, a sequence — all can be folded over in the
same way. Any collection is foldable so long as it supports the
deconstruction operation, which tells if the collection is empty, or
gives its element and the rest of the sequence. One is tempted to
abstract again — this time not over a mere type like int or int list, but over a type constructor such as list, and introduce

    type ('a,'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}

This is a hypothetical OCaml: the type variable ‘F (with the
upper-case name) is to be instantiated not with types but one-argument
type constructors: technically, one says it has the higher-kind
* -> * rather than the ordinary kind * of types and ordinary type variables
such as 'a. The record seq is, hence, higher-kind polymorphic. The
function foldm then generalizes to

    let rec folds (m: 'a monoid) (s: ('a,'F) seq) : 'a 'F -> 'a = fun c ->
        match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)

Again, 'F is instantiated not with just any type constructor, but only that
for which we can find the value ('a,'F) seq; thus folds exhibits
bounded higher-kinded polymorphism.

Alas, higher-kind type variables are not possible in OCaml. The
next section explains why. The following sections tell what we can do in
OCaml instead. There are several alternatives. In some, the end result
ends up looking almost exactly as the above imagined
higher-kind–polymorphic code.

Why higher-kinded polymorphism is not supported directly in OCaml

Higher-kind type variables are not supported in OCaml. Yallop and
White’s FLOPS 2014 paper (Sec. 1.1) explains why: in a word, type
aliasing. For completeness, we recount their explanation here, with
modifications.

Consider the following two modules:

    module Tree = struct
      type 'a t = Leaf | Branch of 'a t * 'a * 'a t
    end
    
    module TreeA : dcont = struct
      type 'a t = ('a * 'a) Tree.t
    end

Here, 'a Tree.t is a data type: a fresh type, distinct from
all other existing types. On the other hand, 'a TreeA.t is an alias:
as its declaration says, it is equal to an existing type, viz. ('a * 'a) Tree.t.

Suppose OCaml had higher-kind * -> * type variables, such as 'F
hypothesized in the previous section. Type checking is, in the end,
solving/checking type equalities, such as 'a 'F = 'b 'G. If
higher-kind type variables ranged only over data type constructors,
the solution is easy: 'a = 'b and 'F = 'G: a data type is fresh, hence
equal only to itself. This is the situation in Haskell. To ensure that
only data type constructors can be substituted for higher-kind type
variables, a Haskell compiler keeps track of type aliases, even across
module boundaries. Module system in Haskell is rather simple, so such
tracking is unproblematic.

Module system of ML is, in contrast, sophisticated. It has functors,
signatures, etc., and extensively relies on type aliases, for example:

    module F(T: sig type 'a t  val empty: 'a t end) = struct
      type 'a ft = 'a T.t
    end

If we preclude substitution of type aliases for higher-kind type
variables, we severely restrict expressiveness. For example, 'a ft
above is a type alias; hence F(TRee).ft cannot be substituted for a
higher-kind type variable, even though one may feel F(TRee).ft is
the same as Tree.t, which is substitutable.

On the other hand, if we allow type aliases to be substituted for
higher-kind type variables, the equivalence of 'a 'F = 'b 'G and 'a = 'b, 'F = 'G breaks down. Indeed, consider (int*int) 'F = int 'G. This equation now has the solution: 'F = Tree.t and 'G = TreeA.t. Parameterized type aliases like 'a TreeA.t are type
functions, and type expressions like int TreeA.t are applications of
those functions, expanding to the right-hand-side of the alias
declaration with 'a substituted for int. Thus, with type aliases,
the type equality problem becomes the higher-order unification problem,
which is not decidable.

References

Jeremy Yallop and Leo White: Lightweight higher-kinded
polymorphism. FLOPS 2014.

Higher-kinded functions as Functors

Although OCaml does not support higher-kind type variables, higher-kinded
polymorphism is not out of the question. There are other ways of
parameterizing by a type constructor: the module system (functor)
abstraction is the first to come to mind.
It is however rather verbose and cumbersome. Let us see.

We now re-write the hypothetical higher-kind–polymorphic OCaml code
at the end of [Introduction] in the real OCaml — by raising the level, so to
speak, from term-level to module-level. The hypothetical record

    type ('a,'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}

becomes the module signature

    module type seq_i = sig
      type 'a t                                (* sequence type *)
      val decon : 'a t -> ('a * 'a t) option
    end

which represents the higher-kind type variable 'F, not supported in
OCaml, with an ordinary type constructor t (type
constant). Different implementations of seq_i (see, e.g., ListS
below) instantiate 'a t in their own ways; hence
t does in effect act like a variable. The hypothetical
higher-kind–polymorphic function

    let rec folds (m: 'a monoid) (s: ('a,'F) seq) : 'a 'F -> 'a = fun c ->
        match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)

becomes the functor, parameterized by the seq_i signature:

    module FoldS(S:seq_i) = struct
      let rec fold (m: 'a monoid) : 'a S.t -> 'a = fun c ->
        match S.decon c with None -> m.unit | Some (h,t) -> m.op h (fold m t)
    end

We got what we wanted: abstraction over a sequence. To use
it to define other higher-kinded polymorphic functions, such as
sums to sum up a sequence, we also
need functors. Functors are infectious, one may say.

    module SumS(S:seq_i) = struct
      open S
      open FoldS(S)
      let sum : int t -> int = fold monoid_plus
    end

Finally, an example of instantiating and using
higher-kind–polymorphic functions: summing a list. First we need an
instance of seq_i for a list: the witness that a list is a sequence.

    module ListS = struct
      type 'a t = 'a list
      let decon = function [] -> None | h::t -> Some (h,t)
    end

which we pass to the SumS functor:

    let 6 =
      let module M = SumS(ListS) in M.sum [1;2;3]

The accompanying code shows another example: using the same SumS to
sum up an array, which also can be made a sequence.

Thus in this approach, all higher-kind–polymorphic functions are
functors, which leads to verbosity, awkwardness and boilerplate. For
example, we cannot even write a SumS application as SumS(ListS).sum [1;2;3]; we have to use the verbose expression above.

References

HKPoly_seq.ml [11K]

The complete code with tests and other examples

Yallop and White’s Lightweight higher-kinded polymorphism

Perhaps surprisingly, higher-kinded polymorphism can always be reduced
to the ordinary polymorphism, as Yallop and White’s FLOPS 2014 paper
cleverly demonstrated. They explained their approach as
defunctionalization. Here we recap it and explain in a different way.

Consider the type 'a list again. It is a parameterized type: 'a is
the type of elements, and list is the name of the collection: `the
base name’, so to speak. The combination of the element type and the
base name can be expressed differently, for example, as
('a,list_name) app, where ('a,'b) app is some fixed type, and
list_name is the ordinary type that tells the base name. The fact
that the two representations are equivalent is witnessed by the
bijection:

    inj: 'a list -> ('a,list_name) app
    prj: ('a,list_name) app -> 'a list

Here is a way to implement it. First, we introduce the dedicated
`pairing’ data type. It is extensible, to let us define as many
pairings as needed.

    type ('a,'b) app = ..

For 'a list, we have:

    type list_name
    type ('a,'b) app += List_name : 'a list -> ('a,list_name) app

In this case the bijection 'a list <-> ('a,list_name) app is:

    let inj x = List_name x and
    let prj (List_name x) = x

and the two functions are indeed inverses of each other.

Exercise: Actually, that the above inj and prj are
the inverses of each other is not as straightforward. It requires a
side-condition, which is satisfied in our case. State it.

In this new representation of the polymorphic list as ('a,list_name) app, the base name list_name is the ordinary (kind *)
type. Abstraction over it is straightforward: replacing with a
type variable. The base-name-polymorphism is, hence, the ordinary
polymorphism. We can then write the desired sequence-polymorphic
folds almost literally as the hypothetical code at the end of [Introduction]:

    type ('a,'n) seq = {decon: ('a,'n) app -> ('a * ('a,'n) app) option}
    
    let rec folds (m: 'a monoid) (s: ('a,'n) seq) : ('a,'n) app -> 'a = fun c ->
        match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)

Instead of 'a 'F we write ('a,'n) app. That’s it. Using folds in
other higher-kinded functions is straightforward, as if it were
a regular polymorphic function (which it actually is):

    let sums s c = folds monoid_plus s c
     (* val sums : (int, 'a) seq -> (int, 'a) app -> int =  *)

Type annotations are not necessary: the type inference works. Here is a
usage example, summing a list:

    let list_seq : ('a,list_name) seq =
      {decon = fun (List_name l) ->
       match l with [] -> None | h::t -> Some (h,List_name t)}
    
    let 6 = sums list_seq (List_name [1;2;3])

There is still a bit of awkwardness remains: the user have to think up
the base name like list_name and the tag like List_name, and
ensure uniqueness. Yallop and White automate using the module system,
see the code accompanying this page, or Yallop and White’s paper (and
the Opam package `higher’).

We shall return to Yallop and White’s approach later on this page,
with another perspective and implementation.

References

Jeremy Yallop and Leo White: Lightweight higher-kinded
polymorphism. FLOPS 2014.

HKPoly_seq.ml [11K]

The complete code with tests and other examples

Sidestepping higher-kinded polymorphism

At times, higher-kinded polymorphism can be avoided altogether: upon
close inspection it may turn out that the problem at hand does not
actually require higher-kinded polymorphism. In fact, our running
example is such a problem.

Let us examine the sequence interface,
parameterized both by the type of the sequence elements and the sequence
itself. The definition that first comes to mind, which cannot be written
as such in OCaml, is (from Introduction):

    type ('a,'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}

It has a peculiarity: the sole operation decon consumes and produces
sequences of the same type 'a 'F (i.e., the same sort of sequence
with the elements of the same type). That is, 'F
always occurs as the type 'a 'F, where 'a is seq‘s parameter: 'a and
'F do not vary independently. Therefore, there is actually
no higher-kinded polymorphism here. The sequence interface can be written
simply as

    type ('a,'t) seq = {decon: 't -> ('a * 't) option}

with folds taking exactly the desired form:

    let rec folds (m: 'a monoid) (s: ('a,'t) seq) : 't -> 'a = fun c ->
        match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)

It is the ordinary polymorphic function. There is no problem in using
it to define other such sequence-polymorphic functions, e.g.:

    let sums s c = folds monoid_plus s c
    (* val folds : 'a monoid -> ('a, 't) seq -> 't -> 'a =  *)

and applying it, say, to a list:

    let list_seq : ('a,'a list) seq =
      {decon = function [] -> None | h::t -> Some (h,t)}
    
    let 6 = sums list_seq [1;2;3]

Exercise: Consider the interface of collections that may be
`mapped’, in the hypothetical OCaml with higher-kind type variables:

    type ('a,'b,'F) ftor = {map: ('a->'b) -> ('a 'F -> 'b 'F)}

Now 'F is applied to different types. Can this interface be still
expressed using the ordinary polymorphism, or higher-kinded
polymorphism is really needed here?

Looking very closely at the higher-kinded polymorphic interface
('a,'F) seq and the ordinary polymorphic ('a,'t) seq, one may
notice that the latter is larger. The higher-kinded interface
describes only polymorphic sequences such as 'a list, whereas
('a,'t) seq applies also to files, strings, buffers, etc. Such an
enlargement is welcome here: we can apply the same folds to
sequences whose structure is optimized for the type of their
elements. In Haskell terms, ('a,'t) seq corresponds to `data
families’, a later Haskell extension. Here is an
example, of applying folds to a string, which is not a polymorphic
sequence:

    let string_seq : (char,int*string) seq =
      {decon = fun (i,s) ->
        if i >= String.length s || i < 0 then None else Some (s.[i], (i+1, s))}
    
    let 'c' = folds monoid_maxchar string_seq (0,"bca")

We can hence use folds with any collection, polymorphic or not, for
which there is an implementation of the ('a,'t) seq interface. We have
encountered the old, and very useful trick: enlarging the type but
restricting the set of its values by having to be able to define `witnesses'
such as ('a,'t) seq.

Exercise: Yallop and White's approach can also deal with
non-polymorphic collections. Use it to implement string_seq.

References

HKPoly_seq.ml [11K]

The complete code with tests and other examples

Algebras

The running example, the seq interface, was about deconstruction of
sequences: technically, about co-algebras. Let us now turn to
construction: building of values using a fixed set of operations,
which can be considered an embedded DSL. The abstraction over a DSL
implementation gives rise to polymorphism. If the embedded
DSL is typed, the polymorphism becomes higher-kinded -- as commonly seen
in DSL embeddings in tagless-final style.

Here we briefly recount how the higher-kinded polymorphism arises in DSL
embeddings, and how it can be hidden away. The key idea is initial
algebra, which is, by definition, the abstraction over any concrete
algebra of the same signature, i.e., the abstraction over DSL implementations.

Our running example in this section is a simple programming language
with integers and booleans: a dialect of the language used in Chap. 3
of Pierce's `Types and Programming Languages' (TAPL). Here is the familiar
tagless-final embedding in OCaml. The grammar of the language is
represented as an OCaml signature:

    module type sym = sig
      type 'a repr
      val int    : int -> int repr
      val add    : int repr -> int repr -> int repr
      val iszero : int repr -> bool repr
      val if_    : bool repr -> 'a repr -> 'a repr -> 'a repr
    end

The language is typed; therefore, the type 'a repr, which represents DSL
terms, is indexed by the term's type: an int or a bool. The
signature sym also defines the type system of the DSL: almost like
in TAPL, but with the typing rules written in a
vertical-space--economic way.

Here is a sample term of the DSL:

    module SymEx1(I:sym) = struct
      open I
      let t1 = add (add (int 1) (int 2)) (int 3) (* intermediate binding *)
      let res = if_ (iszero t1) (int 0) (add t1 (int 1))
    end

It is written as a functor parameterized by sym: a DSL
implementation is abstracted out. The term is polymorphic over
sym and, hence, may be evaluated in any implementation of the DSL. Since
sym contains a higher-kinded type repr, the polymorphism is
higher-kinded.

The just presented (tagless-final) DSL embedding followed the
approach described in [Higher-kinded functions as Functors]. Let us move away from functors
to ordinary terms. Actually, we never quite escape functors, but we
hide them in terms, relying on first-class modules.
As we have seen, a DSL term of the type int such as SymEx1 is the functor

    functor (I:sym) -> sig val res : int I.repr end

To abstract over int, we wrap it into a module

    module type symF = sig
      type a
      module Term(I:sym) : sig val res : a I.repr end
    end

which can then be turned into ordinary polymorphic type:

    type 'a sym_term = (module (symF with type a = 'a))

which lets us represent the functor SymEx1 as an ordinary OCaml value:

    let sym_ex1 : _ sym_term = 
      (module struct type a = int module Term = SymEx1 end)

Here, the type annotation is needed. However, we let the type of the term
to be _, as a schematic variable. OCaml infers it as int.
If we have an implementation of sym, say, module R, we can use it
to run the example (and obtain the sym_ex1's value in R's interpretation):

    let _ = let module N = (val sym_ex1) in 
            let module M = N.Term(R) in M.res

The type 'a sym_term can itself implement the sym signature, in
a `tautological' sort of way:

    module SymSelf : (sym with type 'a repr = 'a sym_term) = struct
      type 'a repr = 'a sym_term
      let int : int -> int repr = fun n ->
        let module M(I:sym) = struct let res = I.int n end in
        (module struct type a = int module Term = M end)
      let add : int repr -> int repr -> int repr = fun (module E1) (module E2) ->
        let module M(I:sym) = 
          struct module E1T = E1.Term(I) module E2T = E2.Term(I)
                 let res = I.add (E1T.res) (E2T.res) 
          end in
        (module struct type a = int module Term = M end)
       ...
    end

That was a mouthful. But writing sym DSL terms becomes much
easier, with no functors and no type annotations. The earlier sym_ex1
can now be written as

    let sym_ex1 = 
      let open SymSelf in
      let t1 = add (add (int 1) (int 2)) (int 3) in (* intermediate binding *)
      if_ (iszero t1) (int 0) (add t1 (int 1))

It can be evaluated in R or other implementation as shown before.

Technically, SymSelf is the initial algebra: an implementation of
the DSL that can be mapped to any other implementation, and in a
unique way. That means its terms like sym_ex1 can be evaluated in
any sym DSL implementation: they are polymorphic over DSL implementation.

On the down-side, we have SymSelf, which is the epitome of
boilerplate: utterly trivial and voluminous code that has to be
written. On the up side, writing DSL terms cannot be easier: no type
annotations, no functors, no implementation passing -- and no overt
polymorphism, higher-kind or even the ordinary kind. Still, the terms
can be evaluated in any implementation of the DSL.

Exercise: Apply Yallop and White's method to this DSL
example. Hint: the first example in Yallop and White's paper, monad
representations, is an example of a DSL embedding in tagless-final
style.

References

HKPoly_tf.ml [13K]

The complete code with tests and detailed development

Initial Algebra

The initial algebra construction using first-class functors,
in the case of one-sorted algebras (corresponding to untyped DSLs)

Stephen Dolan: phantom type. Message on the caml-list
posted on Mon, 27 Apr 2015 12:51:11 +0100

What's in a higher-kinded type name

We now look back at Yallop and White's approach of reducing
higher-kinded polymorphism to the ordinary polymorphism, from a
different perspective. It gives if not a new insight, at least new
implementations.

A polymorphic type like 'a list represents a family of types,
indexed by a type (of list elements, in this example). A higher-kinded
type abstraction such as 'a 'F with the hypothetical (in OCaml)
higher-kind type variable 'F is the abstraction over a family name,
so to speak, while still keeping track of the index. Here is another
way of accomplishing such an abstraction.

Consider the existential type exists a. a list (realizable in OCaml
in several ways, although not in the shown notation. We will keep the
notation for clarity). The existential is now the ordinary, rank *
type and can be abstracted in a type variable, e.g., 'd. The `family
name' is, hence, the family type with the hidden index. We have
lost track of the index, however. Therefore, we tack it back, ending
up with the type ('a,'d) hk. Thus (t,exists a. a list) hk is meant
to be the same as t list (for any type t).

There is a problem however: ('a,'d) hk is a much bigger type. We
need the condition that in (t,exists a. a list) hk, the index t is
exactly the one that we hid in the existential quantification -- we
need dependent pairs, not supported in OCaml. Remember the old trick,
however: we may have a bigger type so long as we control the producers
of its values and ensure only the values satisfying the condition are
built. To be concrete, we must make certain that the only way to
produce ('a,'d) hk values is by using functions like inj: 'a list -> ('a, exists a. a list) hk that expose the same index they hide.
At some point the type checker will demand a
proof: when implementing the
inverse mapping ('a, exists a. a list) hk -> 'a list and extracting
the list out of the existential. There are several ways of going about
the proof.

The simplest is to give our word -- that the condition always holds for
all ('a,'d) hk values actually produced, and we have a proof of that
on some piece of paper or in a .v file. This leads to the exceptionally
simple implementation, which does nothing at all
(all of its operations are the identity).

    module HK : sig
      type ('a,'d) hk                       (* abstract *)
      module MakeHK : functor (S: sig type 'a t end) -> sig
        type anyt                           (* also abstract *)
        val inj : 'a S.t -> ('a,anyt) hk
        val prj : ('a,anyt) hk -> 'a S.t
      end
     end = struct
      type ('a,'d) hk = 'd
      module MakeHK(S:sig type 'a t end) = struct
        type anyt = Obj.t
        let inj : 'a S.t -> ('a,anyt) hk = Obj.repr
        let prj : ('a,anyt) hk -> 'a S.t = Obj.obj
      end
    end

The accompanying code shows a different, also quite simple
implementation without any Obj magic.

After enriching the sym signature of the DSL from the previous
section with fake higher-kinded types:

    module type sym_hk = sig
      include sym
      include module type of HK.MakeHK(struct type 'a t = 'a repr end)
    end

we can write the earlier SymEx1 example as a function (a term)
rather than a functor:

    let sym_ex1 (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk =
      let open I in
      let t1 = add (add (int 1) (int 2)) (int 3) |> inj in (* intermediate term *)
      let res = if_ (iszero t1) (int 0) (add t1 (int 1)) in
      inj res

It can be evaluated simply as

    sym_ex1 (module RHK) |> RHK.prj

where RHK is a module implementing sym_hk. Incidentally, if SHK
is another module implementing sym_hk and we attempt
sym_ex1 (module RHK) |> SHK.prj, we discover that
(int,RHK.anyt) bk and (int,SHK.anyt) bk are actually different
types. Although HK does not do anything (at runtime), it does
maintain safety and soundness.

References

HKPoly_tf.ml [13K]

The complete code with tests and detailed development

Conclusions

We have surveyed various ways of abstracting over a type
constructor -- or, writing interface-parameterized terms
when the interface involves a polymorphic type. Even if the
language does not support type-constructor--polymorphism directly,
such interface parameterization can still be realized, as:

• interface abstraction as a functor abstraction
• reducing higher-kinded polymorphism to ordinary polymorphism,
  by establishing a bijection between type constructors and
  ordinary types
• hiding the polymorphism over DSL implementations
  behind initial algebra
  (if the interface is algebraic, as often happens in tagless-final
  DSL embeddings)
• and in some problems, higher-kinded polymorphism is not actually
  needed, on close inspection