# Higher kinded polymorphism

**URL:** <https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192>\
**Category:** Learning\
**Created:** [June 23, 2018, 6:06pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192 "2018-06-23T18:06:36Z")\
**Posts on this page:** 14\
**Page:** 1

<div class="post-metadata">

**Author:** ![theindigamer](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/theindigamer/32/610_2.png) [@theindigamer](https://discuss.ocaml.org/u/theindigamer)\
**Post date:** [June 23, 2018, 6:06pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/1 "2018-06-23T18:06:36Z")

</div>

I was reading the “[Lightweight Higher-Kinded Polymorphism](https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf)” paper and I couldn’t quite understand the motivation section (I’m familiar with Haskell).

> In Haskell data and newtype definitions create fresh data types. It is possible  
> to hide the data constructors of such types by leaving them out of the export list  
> of the defining module, but the **association between a type name and the data  
> type it denotes cannot be abstracted**. [emphasis mine]

Is this related to/a consequence of:

1. The fact that you cannot hide type aliases but you can do so for newtypes/data?
2. When GHC is typechecking a module, and it looks at an imported type, it can and will deduce whether the name corresponds to a type alias or to a newtype/data?

Looking at the “ilist/iplist” example in the paper, I don’t quite understand what the problem is – if there is no most general type that `'a 'f` can be unified with, shouldn’t that be a type error? Alternatively, what’s wrong with using the obvious solution? I wasn’t even sure of how to come up with an example in Haskell describing the same problem in an attempt to see what GHC does when it encounters a similar situation. AFAICT, Haskell never infers types to correspond to aliases (they must be explicitly annotated or derived indirectly from an annotation).

If someone can give another example illustrating the problem, that’d be very helpful.

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [June 25, 2018, 7:36pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/2 "2018-06-25T19:36:21Z")

</div>

I came up with an example that demonstrates my understanding of the issue. The goal is to construct an example where always choosing either of the two possible solutions for the unification problem makes the program ill-typed (so we can see there is no _most general_ solution).

First, let’s introduce a higher-kinded function. Since OCaml doesn’t have first-class higher-kinded polymorphism, we use a functor (the “heavyweight” higher-kinded polymorphism):

```ocaml
module Fold2 (T1 : sig type 'a t end) (T2 : sig type 'a t end) : sig
  val f : (('a -> 'b -> 'b) -> 'c T1.t -> 'b -> 'b) ->
    (('a -> 'b -> 'b) -> 'c T2.t -> 'b -> 'b) ->
    ('a -> 'a -> 'b -> 'b) ->
    'c T1.t -> 'c T2.t -> 'b -> 'b
end = struct
  let f f1 f2 f c1 c2 = f1 (fun e1 -> f2 (f e1) c2) c1
end

```

Basically it’s a fold over cross-product of the elements of two containers, but the type parameters of the container types (`'c`), though are equal, _don’t necessarily correspond_ to the element type (although are same in both containers).

Now let’s introduce some useful type that makes use of this relaxed constraint. We choose it to be a synonym that is seen as an abstract type from the outside of the module so that the parameter becomes phantom and expresses some additional invariant (constraint) on the state of the container (rather than expressing the type of the element). For example, we can encode emptiness of a set of integers so that

```auto
empty set + empty set = empty set
empty set + nonempty set = nonempty set
nonempty set + nonempty set = nonempty set

empty set x empty set = empty set
empty set x nonempty set = empty set
nonempty set x nonempty set = nonempty set

```

where `x` is the Cartesian product of the sets:

```ocaml
type (+'s0, +'p0) empty =
  <
    name : [`empty];
    plus_empty : ('s0, 'p0) empty;
    plus_nonempty : ('s0, 'p0) nonempty;
    times_empty : ('s0, 'p0) empty;
    times_nonempty : ('s0, 'p0) empty
  > * ('s0 * 's1) * ('p0 * 'p1)
  constraint 's0 = < plus_empty : 's1; plus_nonempty : _; .. > * _ * _
  constraint 'p0 = < times_empty : 'p1; times_nonempty: _; .. > * _ * _
  and (+'s0, +'p0) nonempty =
    <
    name : [`nonempty];
    plus_empty : ('s0, 'p0) nonempty;
    plus_nonempty : ('s0, 'p0) nonempty;
    times_empty : ('s0, 'p0) empty;
    times_nonempty : ('s0, 'p0) nonempty;
    > * ('s0 * 's1) * ('p0 * 'p1)
  constraint 's0 = < plus_nonempty : 's1; plus_empty: _; .. > * _ * _
  constraint 'p0 = < times_nonempty :'p1; times_empty: _; .. > * _ * _

module Int_set : sig
  type +'a t
  val empty : (_ empty) t
  val single : int -> (_ nonempty) t
  val choose : (_ nonempty) t -> int
  val sum : 'a t -> (_ * ('a * 'b) * _) t -> 'b t
  val xprod : (int -> int -> int) -> 'a t -> (_ * _ * ('a * 'b)) t -> 'b t
  val intersects : 'a t -> 'b t -> bool
  val fold : (int -> 'b -> 'b) -> 'a t -> 'b -> 'b
end = struct
  module Int_set = Set.Make (struct type t = int let compare : int -> _ = compare let equal : int -> _ = (=) end)
  open Int_set
  type nonrec +'a t = t
  let empty = empty
  let single = singleton
  let choose = choose
  let sum = union
  let fold = fold
  module F = Fold2 (struct type 'a t = Int_set.t end) (struct type 'a t = Int_set.t end)
  let xprod f a b = F.f fold fold (fun e1 e2 -> add @@ f e1 e2) a b empty
  let intersects a b = F.f fold fold (fun e1 e2 acc -> acc || e1 = e2) a b false
end

```

Now let’s try to do the same for lists of integers, but extend the module with three extra “useful” (the example is still somewhat artificial) functions:

```ocaml
  val intersects1 : 'a Int_set.t -> 'b t -> bool
  val intersects2 : int list -> 'b t -> bool
  val intersects3 : int list -> string list -> bool

```

where the type `'a t` is the type of integer lists with a phantom parameter indicating emptiness:

```ocaml
module Int_list : sig
  type +'a t
  val empty : (_ empty) t
  val single : int -> (_ nonempty) t
  val choose : (_ nonempty) t -> int
  val sum : 'a t -> (_ * ('a * 'b) * _) t -> 'b t
  val xprod : (int -> int -> int) -> 'a t -> (_ * _ * ('a * 'b)) t -> 'b t
  val intersects : 'a t -> 'b t -> bool
  val fold : (int -> 'b -> 'b) -> 'a t -> 'b -> 'b

  val intersects1 : 'a Int_set.t -> 'b t -> bool
  val intersects2 : int list -> 'b t -> bool
  val intersects3 : int list -> string list -> bool
end = struct
  open List
  type +'a t = int list
  let empty = []
  let single a = [a]
  let choose = hd
  let sum = (@)
  let fold = fold_right
  module F = Fold2 (struct type 'a t = int list end) (struct type 'a t = int list end)
  let xprod f a b = F.f fold fold (fun e1 e2 acc -> f e1 e2 :: acc) a b []
  let f e1 e2 acc = acc || e1 = e2
  let intersects a b = F.f fold fold f a b false

  module F' = Fold2 (struct type 'a t = 'a Int_set.t end) (struct type 'a t = int list end)
  module F'' = Fold2 (struct type 'a t = int list end) (struct type 'a t = 'a list end)

  let intersects1 : type a b. a Int_set.t -> b t -> bool = fun a b -> F'.f Int_set.fold fold f a b false
  let intersects2 a b = F''.f fold fold f a b false
  let intersects3 a b = F''.f fold (fun f -> fold @@ fun x -> f @@ int_of_string x) f a b false
end

```

Here, at last, we can see the problem. Since we used the OCaml’s “heavyweight” functors, we were able to precisely indicate how to perform the higher-order unification in presence of type synonyms (the functor applications resulting in modules `F'` and `F''`). If we try to change either of the exactly specified solutions (try to exchange `int list` \<–\> `'a list` in the second parameter of the functor applications), we get a type error. You can just try it to see exactly which those errors are in both cases. So this example just tangibly demonstrates that neither of the solutions is more general than the other one.

Now I intentionally used rigid type variables in the definition of `intersects1` to expose the problem with Haskell approach as I understand it (rigid type variables allow to simulate Haskell approach to specifying type signatures and avoid possible signature inclusion check failure). Basically, Haskell doesn’t treat type synonyms as first-class types and always expands them until it obtains applications of type constructors (datatypes). Then there’s no ambiguity, but just the second solution is always chosen _by definition_ (no first-class support for type synonyms). So we can expect the same error as if we replace `type 'a t = int list` with `type 'a t = 'a list` in the second argument of `Fold2` for module `F'`. I tried to simulate this situation with GHCi (I have less experience with Haskell, so no real implementation of set with a phantom type, just a dummy datatype definition with a phantom parameter) and indeed obtained the following error:

```haskell
:set -XRankNTypes
:{
let f :: forall t1 t2 a b c. ((a -> b -> b) -> t1 c -> b -> b)
         -> ((a -> b -> b) -> t2 c -> b -> b)
         -> (a -> a -> b -> b)
         -> t1 c -> t2 c -> b -> b
    f f1 f2 f c1 c2 = f1 (\e1 -> f2 (f e1) c2) c1
:}

data IntSet a = IntSet [Int]
type T a = [Int]

:{
let foldr :: (Int -> b -> b) -> T a -> b -> b
    foldr k = go
      where
        go [] z = z
        go (y:ys) z = y `k` go ys z
:}
:{
let foldrIntSet :: (Int -> b -> b) -> IntSet a -> b -> b
    foldrIntSet f (IntSet l) = foldr f l
:}

:{
let intersect :: T a -> T b -> Bool
    intersect a b = f foldr foldr (\e1 e2 -> (|| e1 == e2)) a b False
:}
:{
let intersect1 :: IntSet a -> T b -> Bool
    intersect1 a b = f foldrIntSet foldr (\e1 e2 -> (|| e1 == e2)) a b False
:}

```

```haskell
<interactive>:31:68: error:
    • Couldn't match type ‘a’ with ‘Int’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          intersect1 :: forall a b. IntSet a -> T b -> Bool
        at <interactive>:30:5-41
      Expected type: IntSet Int
        Actual type: IntSet a
    • In the fourth argument of ‘f’, namely ‘a’
      In the expression:
        f foldrIntSet foldr (\ e1 e2 -> (|| e1 == e2)) a b False
      In an equation for ‘intersect1’:
          intersect1 a b
            = f foldrIntSet foldr (\ e1 e2 -> (|| e1 == e2)) a b False
    • Relevant bindings include
        a :: IntSet a (bound at <interactive>:31:16)
        intersect1 :: IntSet a -> T b -> Bool (bound at <interactive>:31:5)

```

It looks very similar to the OCaml analogue (when we use rigid type variables and choose the wrong solution in `F'`):

```auto
This expression has type a Int_set.t
       but an expression was expected of type int Int_set.t
       Type a is not compatible with type int

```

Edit: typos, better Haskell formatting

---

<div class="post-metadata">

**Author:** ![theindigamer](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/theindigamer/32/610_2.png) [@theindigamer](https://discuss.ocaml.org/u/theindigamer)\
**Post date:** [June 29, 2018, 12:21am UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/3 "2018-06-29T00:21:38Z")

</div>

Thanks for taking the time to write a detailed explanation! Unfortunately, after re-reading it multiple times, I’m still not certain of what exactly the OCaml code is doing. For example, what do the `_` in the type signatures do?

Also, I’m not sure what the final conclusion is 😕 ? I would’ve thought that it would be something like “with Haskell, in situation X, higher-kinded polymorphism doesn’t cause a problem, but when you try encoding the same in OCaml in a ‘lightweight manner’, the compiler cannot deduce types because the OCaml type-checker has to consider the possibility Y which Haskell doesn’t because of Z reasons” but you seem to have demonstrated something different where the same problem arises in both OCaml and Haskell 😅.

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [June 29, 2018, 6:34am UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/4 "2018-06-29T06:34:40Z")

</div>

I think the final conclusion is simply that due to this issue with higher-order unification it’s not possible to have both _implicit_ type abstraction (i.e. without any annotations e.g. in the form of type coercions/wrapper constructors) and _implicit_ higher-kinded polymorphism (i.e. without any annotations e.g. in the form of functor instantiations). Somewhere you’ll have to provide solutions manually. And Haskell vs OCaml make different choices here. I actually came up with a complete Haskell implementation of my example [here](https://gist.github.com/schrodibear/d6251a87e49e2a5b4ea29fee755d103b). The thing to note about the implementation is that it uses coercions/constructors/pattern matches to wrap/unwrap the parametrized types `IntSet a`/`IntList a` to/from their monomorphic representations `Set Int` and `[Int]`. In OCaml I don’t have to explicitly wrap/unwrap anything, inside the modules the types `'a t` and `int list` are fully interchangeable while outside, even if I expose the representation as e.g. `type +a t = private int list`, they will be treated as distinct (incompatible). In Haskell if I want a distinct type I have to use coercions everywhere, both inside the module and outside of it. But in OCaml I have to use functors or some special encoding to achieve higher-kinded polymorphism, while in Haskell it’s supported directly.

---

<div class="post-metadata">

**Author:** ![lpw25](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/lpw25/32/144_2.png) [@lpw25](https://discuss.ocaml.org/u/lpw25)\
**Post date:** [June 29, 2018, 6:38am UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/5 "2018-06-29T06:38:20Z")

</div>

I wrote the description in the paper, so you’ve already read my best efforts to explain this, but I’ll have another go.

In Haskell, if you have a type `Foo Int` you know that there is no type `Bar Int` that will be equal to it. The newtypes/datatypes `Foo` and `Bar` are fresh types that do not overlap.

You could create a type alias `type Baz x = Foo x` but since that alias can never have its definition hidden we can just always expand them away and never consider them as candidates for higher-kinded polymorphism.

This freshness restriction means that if you need to unify `Foo Int` with `m Int` you can always just say that `Foo = m` without any loss of generality.

In OCaml, if you see `int foo` and `int bar` they may well be equal, even though `foo` and `bar` themselves might not be. For example,

```
type 'a foo = 'a * int
type 'a bar = int * 'a

```

In this case, if you need to unify `int foo` with `int 'm` (assuming we had higher-kinded variables) you can not just make `'m = foo` because `'m = bar` would also be a valid solution and neither one is more general than the other – there is no “best” answer and making an arbitrary choice will mean that your type inference’s success is dependent on arbitrary implementation details of your inference algorithm.

So without the freshness restriction of Haskell you cannot have simple higher-kinded polymorphism. However, there are costs to the restriction as well. Support for modular abstraction (i.e. functors in OCaml) requires the ability to have multiple names for the same thing – the parameter of a functor will be equal to the functor’s arguments – and this does not play nicely with these kinds of freshness restrictions.

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [June 29, 2018, 7:02am UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/6 "2018-06-29T07:02:38Z")

</div>

For the type signatures I just wanted to show an example where having a synonym `type a t = int list` with a phantom parameter can be “useful” or, at least, meaningful. I could have used the number of elements in the set as type-level number or some other trick… But since OCaml doesn’t have type families (that fit for Haskell implementation in such cases) or dependent types one has to somehow partially simulate those features to encode some type-level functions in order to assign meaning to these phantom type parameters. The `_` in signatures just means a fresh type variable, it is used to avoid having to come up with lots of fresh names e.g. `'a0`, `'a1`, `'a2`… I used an extension of the trick described [here](https://inbox.ocaml.org/caml-list/CAAxsn=H62R8eooPkgGJwsQ6Mozi+HuLaE95UzOBbxLiF1fd0nw@mail.gmail.com/) to encode the equations for type-level operations on the types `empty` and `nonempty`.

---

<div class="post-metadata">

**Author:** ![jhw](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/jhw/32/1639_2.png) [@jhw](https://discuss.ocaml.org/u/jhw)\
**Post date:** [June 29, 2018, 12:59pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/7 "2018-06-29T12:59:50Z")

</div>

Thanks for that explanation. It’s the first time I’ve seen an explanation for something that I had only had an intuition about before.

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [June 29, 2018, 1:49pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/8 "2018-06-29T13:49:38Z")

</div>

> [@lpw25](#):
>
> For example,
> 
> ```auto
> type 'a foo = 'a * int
> type 'a bar = int * 'a
> 
> ```
> 
> In this case, if you need to unify `int foo` with `int 'm` (assuming we had higher-kinded variables) you can not just make `'m = foo` because `'m = bar` would also be a valid solution and neither one is more general than the other – there is no “best” answer

One subtlety about this is that actually when we have both of the equations in scope, then either of the solutions _is_ the most general, they are both convertible in both directions. To really expose the problem (find a program that will not typecheck with at least one of the solutions) one needs to find a program where some parameters occur not only inside the type abbreviations themselves, but also in other types, that are _not_ abbreviations or that have no associated equalities in scope. And constructing some meaningful example where this actually happens turned out to be not that simple, at least for me. In my example the parameter `'a` occurs in either both `'a Int_list.t` and `'a Int_set.t` or both `'a Int_list.t` and `'a list`. In this case there’s indeed no most general type, but in many simpler cases type inference succeeds both ways with the same solutions.

---

<div class="post-metadata">

**Author:** ![lpw25](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/lpw25/32/144_2.png) [@lpw25](https://discuss.ocaml.org/u/lpw25)\
**Post date:** [June 29, 2018, 2:42pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/9 "2018-06-29T14:42:43Z")

</div>

Unless I’m misunderstanding you, then (assuming OCaml had higher-kinded variables) considering:

```
let foo : 'm. int 'm -> float 'm option = fun _ -> None
let bar : int foo = 1, 2
let result = foo bar

```

is sufficient to see that both solutions are not equivalent. If you go one way then you get `result : (int * float) option` if you go the other way then you get `result : (float * int) option`. These are clearly not instances of each other.

This example relies on me not giving `foo` it’s most general type, but you can fairly easily make longer examples where that’s not the case, and this example should be enough to see where the problem lies.

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [June 29, 2018, 4:07pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/10 "2018-06-29T16:07:35Z")

</div>

Indeed. By manually constraining the types it’s possible to construct much smaller examples. I also think another reason why Haskell approach doesn’t work for OCaml is that OCaml has type synonyms that don’t have a canonical form, e.g.

```ocaml
type ('a, 'b) t = [`A of 'a | `B of 'b]

```

Even if we choose to always expand all synonyms

```ocaml
'a 't ~ [`A of int | `B of string]

```

already has many solutions without the most general one.

---

<div class="post-metadata">

**Author:** ![cfcs](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/cfcs/32/833_2.png) [@cfcs](https://discuss.ocaml.org/u/cfcs)\
**Post date:** [June 29, 2018, 4:55pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/11 "2018-06-29T16:55:55Z")

</div>

is the `~` above part of the type expression language?

---

<div class="post-metadata">

**Author:** ![schrodibear](https://avatars.discourse-cdn.com/v4/letter/s/958977/32.png) [@schrodibear](https://discuss.ocaml.org/u/schrodibear)\
**Post date:** [June 29, 2018, 5:08pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/12 "2018-06-29T17:08:51Z")

</div>

No, just to designate a unification problem, similar to Haskell’s equality constraint `~` (in Haskell it is a part of type expression language).

---

<div class="post-metadata">

**Author:** ![theindigamer](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/theindigamer/32/610_2.png) [@theindigamer](https://discuss.ocaml.org/u/theindigamer)\
**Post date:** [June 30, 2018, 9:42pm UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/13 "2018-06-30T21:42:44Z")

</div>

Ah, now it makes a lot more sense to me now. Thanks!

> […] the parameter of a functor will be equal to the functor’s arguments – and this does not play nicely with these kinds of freshness restrictions.

Is this somehow related to the discussion on generative vs. applicative functors where having fresh types generated is sometimes bad for code reuse?

---

<div class="post-metadata">

**Author:** ![lpw25](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/lpw25/32/144_2.png) [@lpw25](https://discuss.ocaml.org/u/lpw25)\
**Post date:** [July 1, 2018, 9:17am UTC](https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/14 "2018-07-01T09:17:15Z")

</div>

It is not particularly related to generative vs applicative functors, these issues come up regardless of whether functors are applicative or generative.