I want to learn the advanced type things, but I don't know where to find this information

I feel like I have a decent grasp of OCaml these days, and I can certainly write useful programs with the language, but sometimes when I dig deep into the standard library or Jane Street libraries, I still see things I don’t understand.

An example from seq.mli in the standard libary

type 'a t = unit -> 'a node
and +'a node =
  | Nil
  | Cons of 'a * 'a t

I don’t know what this +'a is. It’s mostly the + I don’t get. Here’s another from Jane Street’s sequence.ml (in Base)

type +_ t = Sequence : 's * ('s -> ('a, 's) Step.t) -> 'a t

I know what _ is in the context of GADTs, but I don’t know what this is. I guess this is also somehow a GADT, but I still don’t understand the +.

Here’s something from stream.ml in the standard library:

let rec dump : type v. (v -> unit) -> v t -> unit = fun f s ->
  print_string "{count = ";
  print_int (count s);
  print_string "; data = ";
  dump_data f (data s);
  print_string "}";
  print_newline ()

What is this v.? It looks like a locally abstracted type, but what is the .?

Can someone direct me to a source of information where I can learn to understand these things with examples?


1 Like

There’s a GADTs section at the OCamlverse learning page, and some of the articles, papers, or books listed there might be relevant.

Some of your questions have answers at the OCamlverse FAQ page, I think.

1 Like

I think it’s worth expanding ninjaaron@'s question. So:

Is there some sort of collection of books/papers, smaller than “the corpus of POPL since 1980” that Ocaml users could consult, to start to understand the background for the Ocaml type system?

I’m putting it this way because (for instance) the syntax bits that ninjaaron@ points at, while I don’t know -precisely- what they mean, and -precisely- the typing rules, are pretty clear to me, and to whatever extent that they aren’t I think I can go dig up the relevant papers/books and understand them. But that’s b/c I spent a decade immersed in The Church of Curry-Howard. I think it might be nice to have a collection of papers that we all collectively think are foundational for understanding the Ocaml type system, so that advanced users like ninjaaron@ could read those to get the same background.

I’m not suggesting a new “advanced users’ manual” or anything like that. Nor even “we should write a paper explaining Ocaml’s type system”. If you’re going to be a user sufficiently advanced to understand local type abstractions, then you’re going to be sufficiently advanced to be able to add up the bits-and-pieces from 3-4 different papers. So for instance, Didier Remy’s paper on record-typing should be in the list. Xavier’s paper on existential types should be there. Heck, Hindley-Milner and Milner-Damas (?) should be there. There are probably others, and I suspect we could come up with a list in short order, just by riffing on “the papers we love about ML-style type theory”.

Possibly there’s a book out there that covers all this: not having lived in these parts the last 20yr, I don’t really know. But even if there were, I think having a list of seminal papers that drove Ocaml’s type system would be valuable, b/c eventually Ocaml evolves, and that book becomes out-of-date, but the list of papers … well, we just add a few more lines to the end, and hey presto! up-to-date!


A while back, I wrote the following for the books section of the OCamlverse learning page mentioned above:

Types and Programming Languages by Benjamin C. Pierce - A friendly but serious book on types, type checking, etc. Much of what’s covered is relevant to OCaml. Several chapters present OCaml implementations of the concepts covered in preceding chapters, and the examples in the book have been typechecked using OCaml programs that are available at the author’s site. (As of mid-2018, the Kindle version can be difficult to read on small devices because the pages are images of the hardcover’s pages. The iBook version is a standard e-book with resizable fonts, though.)

It probably doesn’t address everything one might wonder about concerning types (I wouldn’t know), but I studied parts of the book, I think it’s a great. Peirce also edited an anthology that could be relevant–also listed in the books section. (I haven’t read anything but the table of contents.)

But your comment was really about collections of papers. There’s start of such a list here, which is also at OCamlverse. It sounds like it would be good to add the papers you mentioned to the list. (It’s easy to contribute to OCamlverse. See the bottom of this page: https://ocamlverse.github.io .)

1 Like

A nice book to get started is http://caml.inria.fr/pub/docs/u3-ocaml/ocaml.pdf


1 Like

@mars0i, I’m aware of Benli’s book, and while I haven’t read it (left the field) I’m sure it’s excellent, b/c he’s an excellent writer. What I really mean, is to have a list of papers, with a short blurb that explains how each paper relates to the Ocaml type system. So for instance, Xavier’s paper on existential types is the basis for the Ocaml module system; Damas-Milner for type-inference over expressions, Didier’s record-typing, for the object-system, etc.


Learning about some advanced feature of the language can be difficult because of the first hurdle: What is this thing (e.g., that + sign) called? How do I search for it online?

A good way to overcome this is to check the grammar of the language in the manual: https://caml.inria.fr/pub/docs/manual-ocaml/language.html

For the + example, you can go to the “type definition” section. And right there you can find the +/- sign and it’s called variance. There are other occurrences of the word variance in the page to give you a short explanation and even a few more keywords to search for (notably “covariant” and “contravariant”).