User Tools

Site Tools


blog:2008:05:23:higher-rank_polymorphism_in_ocaml

Higher-Rank Polymorphism in OCaml

How to simulate higher-rank polymorphism in OCaml ?

OCaml type-inference algorithm only allow for prenex (or rank-1) polymorphism. This means that polymorphic generalisation is restricted to full let-bound terms, and not available for function arguments (see Polymorphism_(computer_science) for a more precise definition).

For example, the type of a function

let map_pair f (p1, p2) = (f p1, f p2)

such that map_pair id (1, 'a') would be well-typed is not expressible. One would need the following type:

val map_pair : ('a. 'a -> 'a) -> ('a * 'b) -> ('a * 'b)

Unfortunately, it is not possible to type the argument f of map_pair with the quantified type ('a. 'a → 'a) in OCaml, even with an explicit type annotation.

let map_pair (f : 'a. 'a -> 'a) (p1, p2) = (f p1, f p2)

is not accepted by the OCaml compiler (syntax error at the dot).

A Solution using Records

A place where the OCaml type system allows types with explicit type quantifiers is in record fields. For example, one can define the type

type r = { f : 'a . 'a -> 'a }

which has a field f with polymorphic type.

Function arguments which we would like to type with ('a. 'a → 'a) can then be replaced by records of type r, with their field f set to the function to use. I.e., instead of writing

let id x = x
let map_pair (f : 'a. 'a -> 'a) (p1, p2) = (f p1, f p2)
let sample = map_pair id (3, true)

which is rejected by the compiler, we can write

let id x = x
type r = { f : 'a. 'a -> 'a }
let map_pair r (p1, p2) = (r.f p1, r.f p2)
let sample = map_pair { f = id } (3, true)

This approach has two drawbacks. First, the call site is polluted by encapsulation in the record, having to wrap each polymorphic function argument inside a record. I have not found a way to use the record only at callee side. For example:

let map_pair f (p1, p2) =
   let r = { f = f } in
   (r.f p1, r.f p2)

results in a (legitimate) type error because the field value in {f = f} has type ('a → 'a) which is less general than field type ('a. 'a → 'a). The code is then somehow uglified by the record wrappings.

Secondly, the wrapping of the polymorphic function argument results in allocation of a record in the caller and indirect access to the function argument in the callee. It is not optimized away by the compiler (even though the function is the first and only field of the record) and results in additional (needless) instructions which reduce performance and augment code size.

Another Solution

If you don't mind passing the same arguments multiple times, you can add as much arguments as necessary to have only monomorphic arguments:

let map_pair f1 f2 (p1, p2) = (f1 p1, f2 p2)
let sample = map_pair id id (1, true)

This may however become quickly inconvenient when dealing with large data structures and the increased number of arguments may alter performance.

Ugly Magic

We can avoid both record wrapping and argument multiplication using Obj.magic to cheat with the type system. This solution may be the most effective, but it completely bypasses the type checker and I would not use it.

let map_pair (f : 'a -> 'a) (p1, p2) =
   (f p1, (Obj.magic f : 'b -> 'b) p2)
let sample = map_pair id (1, true)

Discussion

Neil Johnson, 2009/02/04 14:31

This is way more easier in Haskell (with -fglasgow-exts) :

mapPair :: (forall a. a -> a) -> (b, c) -> (b, c)
mapPair f (p1, p2) = (f p1, f p2)
Sarcastic Johnson, 2013/02/22 17:36

This is way more easier with emacs (with M-x make-my-program-in-haskell-which-is-a-better-progamming-language)

Sarcastic Jonsonn, 2013/02/22 17:37

You can emulate this in Vi (with :emacs-haskel-trololol)

Enter your comment. Wiki syntax is allowed:
 
blog/2008/05/23/higher-rank_polymorphism_in_ocaml.txt · Last modified: 2011/02/20 20:28 (external edit)