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

Sacker

I"m not 100% sure, since I don't know Haskell and I'm unclear on what Compose f g x =... actually means in Haskell, but you might be interested to know that the development version of OCAML has first class modules. – Mardis

I'm pretty sure you can't do this in ML, because you need higher-kinded polymorphism. Can you give some examples of how you would use these types in Haskell? – Candide

nlucaroni, very interesting! (The link is caml.inria.fr/cgi-bin/viewcvs.cgi/ocaml/branches/fstclassmod I believe) Chris Conway, I added some examples. – Sacker

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.

Hengelo

Well, Ocaml was first released in 1996, at which time the let-polymorphism restriction was an easy way to ensure complete type inference and principal typing. I don't know what your reference for 'quite easy' is, but type reconstruction for rank-2 polymorphism was only found in 1999. And of course it's undecidable for rank-3 and higher (ibid). – Suffocate

@huitseeker: The question is not about rank-2 types (where you nest the forall quantifier in Haskell), but about higher-order types (where you nest ->). – Sacker

The “deep reason” is explained here, here, and in Section 1.1 The alias problem on page 2 of Lightweight Higher-kinded Polymorphism. Refinement (of the abstract type) model of HKT in Scala’s DOT, also exhibited the inference problem. Abstract dependent types encapsulate to the type of the signature. – Eboat

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

Alica

Please, add a module corresponding to the Fix type constructor of the question. – Nephology

Answer 3

Well... I'm not an expert of higher-order-types nor Haskell programming. But this seems to be ok for F# (which is OCaml), could you work with these:

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

The last one I wrapped to tuple as I didn't come up with anything better...

Equities

However, I meant something like (list, option, int) compose which would be equivalent to (int option) list. – Sacker

I think that this could be done using option types. In F# you could also in .NET-way use multiple type params: type compose<'f, 'g, 'x> = Compose of ('f -> 'g -> 'x);; but this may not be true OCaml syntax. – Equities

Answer 4

You can do it but you need to make a bit of a trick:

newtype Fix f = In{out:: f (Fix f)}

You can define Cata afterwards:

Cata :: (Functor f) => (f a -> a) -> Fix f -> a
Cata f = f.(fmap (cata f)).out

That will define a generic catamorphism for all functors, which you can use to build your own stuff. Example:

data ListFix a b = Nil | Cons a b
data List a = Fix (ListFix a)
instance functor (ListFix a) where
fmap f Nil = Nil
fmap f (Cons a lst) = Cons a (f lst)

Whimsy

The question is about Ocaml's functors (different than Haskell's functors). – Sacker

Sorry, i misread the question. In any case, hope this helps whoever comes into contact with it – Whimsy