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)

when is the superbowl this year what time does the superbowl start tonight click for super bowl 2017 location 2017 super bowl date 51 super bowl sunday 2017 have the panthers won a super bowl who won the superbowl superbowl date 2017 superbowl 2017 date super bowl sunday 2016 date super bowl predictions 2017 super bowl odds 2017 super bowl 2019 date super bowl sunday 2017 thesuperbowlcommercials.org