blog:2008:05:23: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 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.

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.

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)

blog/2008/05/23/higher-rank_polymorphism_in_ocaml.txt · Last modified: 2011/02/20 20:28 (external edit)

Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International

## Discussion

This is way more easier in Haskell (with

`-fglasgow-exts`

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

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