Higher-order type constructors and functors in Ocaml

Question

Can the following polymorphic functions

let id x = x;;
let compose f g x = f (g x);;
let rec fix f = f (fix f);;     (*laziness aside*)

be written for types/type constructors or modules/functors? I tried

type 'x id = Id of 'x;;
type 'f 'g 'x compose = Compose of ('f ('g 'x));;
type 'f fix = Fix of ('f (Fix 'f));;

for types but it doesn't work.

Here's a Haskell version for types:

data Id x = Id x
data Compose f g x = Compose (f (g x))
data Fix f = Fix (f (Fix f))

-- examples:
l = Compose [Just 'a'] :: Compose [] Maybe Char

type Natural = Fix Maybe   -- natural numbers are fixpoint of Maybe
n = Fix (Just (Fix (Just (Fix Nothing)))) :: Natural   -- n is 2

-- up to isomorphism composition of identity and f is f:
iso :: Compose Id f x -> f x
iso (Compose (Id a)) = a

Answer 1

Haskell allows type variables of higher kind. ML dialects, including Caml, allow type variables of kind "*" only. Translated into plain English,

• In Haskell, a type variable g can correspond to a "type constructor" like Maybe or IO or lists. So the g x in your Haskell example would be OK (jargon: "well-kinded") if for example g is Maybe and x is Integer.

• In ML, a type variable 'g can correspond only to a "ground type" like int or string, never to a type constructor like option or list. It is therefore never correct to try to apply a type variable to another type.

As far as I'm aware, there's no deep reason for this limitation in ML. The most likely explanation is historical contingency. When Milner originally came up with his ideas about polymorphism, he worked with very simple type variables standing only for monotypes of kind *. Early versions of Haskell did the same, and then at some point Mark Jones discovered that inferring the kinds of type variables is actually quite easy. Haskell was quickly revised to allow type variables of higher kind, but ML has never caught up.

The people at INRIA have made a lot of other changes to ML, and I'm a bit surprised they've never made this one. When I'm programming in ML, I might having higher-kinded type variables. But they aren't there, and I don't know any way to encode the kind of examples you are talking about except by using functors.

Answer 2

You can do something similar in OCaml, using modules in place of types, and functors (higher-order modules) in place of higher-order types. But it looks much uglier and it doesn't have type-inference ability, so you have to manually specify a lot of stuff.

module type Type = sig
  type t
end

module Char = struct
  type t = char
end

module List (X:Type) = struct
  type t = X.t list
end

module Maybe (X:Type) = struct
  type t = X.t option
end

(* In the following, I decided to omit the redundant
   single constructors "Id of ...", "Compose of ...", since
   they don't help in OCaml since we can't use inference *)

module Id (X:Type) = X

module Compose
  (F:functor(Z:Type)->Type)
  (G:functor(Y:Type)->Type)
  (X:Type) = F(G(X))

let l : Compose(List)(Maybe)(Char).t = [Some 'a']

module Example2 (F:functor(Y:Type)->Type) (X:Type) = struct
  (* unlike types, "free" module variables are not allowed,
     so we have to put it inside another functor in order
     to scope F and X *)
  let iso (a:Compose(Id)(F)(X).t) : F(X).t = a
end