1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
#+TITLE: Writing a Function Whose Argument is a Polymorphic Function in OCaml
#+SERIES: ../miscellaneous.html
#+SERIES_PREV: ./DiscoveringCommonLisp.html
#+BEGIN_EXPORT html
<div id="history">site/posts/RankNTypesInOCaml.org</div>
#+END_EXPORT
In OCaml, it is not possible to write a function whose argument is a
polymorphic function. Trying to write such a function results in the
type-checker complaining back at you.
#+begin_src ocaml :results verbatim :exports both
let foo (type a b) id (x : a) (y : b) = (id x, id y)
#+end_src
#+RESULTS:
: Line 1, characters 50-51:
: 1 | let foo (type a b) id (x : a) (y : b) = (id x, id y);;
: ^
: Error: This expression has type b but an expression was expected of type a
When OCaml tries to type-check ~foo~, it infers ~id~ expects an
argument of type ~a~ because of ~id x~, then fails when trying to
type-check ~id y~.
The trick to be able to write ~foo~ is to use records. Indeed, while
the argument of a function cannot be polymorphic, the field of a
record can. This effectively makes it possible to write ~foo~, at the
cost us a level of indirection.
#+begin_src ocaml :results verbatim :exports code
type id = {id : 'a. 'a -> 'a}
let foo {id} x y =
(id x, id y)
#+end_src
From a runtime perspective, it is possible to tell OCaml to remove the
introduced indirection with the ~unboxed~ annotation. There is nothing
we can do in the source, though. We need to destruct ~id~ in ~foo~,
and we need to construct it at its call-site.
#+begin_src ocaml :exports code
g {id = fun x -> x}
#+end_src
As a consequence, this solution is not a silver bullet, but it is an
option that is worth considering if, /e.g./, it allows to export a
cleaner API to the consumer of a module[fn::Personally, I have been
considering this trick recently to remove the need for a library to be
implemented as a functor].
|