functional programming - 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 enjoy 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.