Higher kinded polymorphism

I was reading the “Lightweight Higher-Kinded Polymorphism” 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.

2 Likes

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

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

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:

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:

  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:

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:

: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
:}
<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'):

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

4 Likes

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 :confused: ? 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 :sweat_smile:.

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

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.

14 Likes

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 to encode the equations for type-level operations on the types empty and nonempty.

1 Like

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.

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.

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.

1 Like

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.

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

Even if we choose to always expand all synonyms

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

already has many solutions without the most general one.

is the ~ above part of the type expression language?

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

1 Like

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?

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