Higher-kinded bounded polymorphism

Higher-kinded polymorphism -- the abstraction over a type constructor to be later supplied with arguments -- is often needed, for expressing generic operations over collections or embedding typed DSLs, particularly in tagless-final style. Typically, the abstracted type constructor is not arbitrary, but must implement a particular interface (e.g., an abstract sequence) -- so-called bounded polymorphism.

OCaml does not support higher-kinded polymorphism directly: OCaml type variables range over types rather than type constructors, and type constructors may not appear in type expressions without being applied to the right number of arguments. Nevertheless, higher-kinded polymorphism is expressible in OCaml -- in fact, in several, more or less cumbersome ways. The less cumbersome ways are particularly less known, and kept being rediscovered. This page summarizes the different ways of expressing, and occasionally avoiding, higher-kinded polymorphism. They are collected from academic papers and messages on the caml-list spread over the years -- and adjusted to fit the story and differently explained.



``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
    module TreeA : dcont = struct
      type 'a t = ('a * 'a) Tree.t
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
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.

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
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)
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

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

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 = <fun> *)
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.

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 = <fun> *)
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.

HKPoly_seq.ml [11K]
The complete code with tests and other examples



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

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 = 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
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)
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.
HKPoly_tf.ml [13K]
The complete code with tests and detailed development



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: