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.

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