Labelled type parameters in OCaml

The OCaml language allows for labelled parameters in function definitions and calls. This is a pleasant feature of the language which can be used to make the code self-documenting. For example consider the difference between the blit functions in the Stdlib.String and Stdlib.StringLabels.

val blit : string -> int -> bytes -> int -> int -> unit
val blit : src:string -> src_pos:int -> dst:bytes -> dst_pos:int -> len:int -> unit

In the second version, the meaning of each parameter is easier to remember and their order is not a source of confusion. And when the function is called, the order of the parameters can be changed:

blit ~len:1024 ~src:s ~src_pos:0 ~dst:b ~dst_pos:0

The OCaml language supports type constructors. But the type parameters cannot be labelled. The meaning and order of each parameter can become a source of confusion. E.g., with the format types from the OCaml Stdlib:

type ('a, 'b, 'c, 'd, 'e, 'f) format6 = ('a, 'b, 'c, 'd, 'e, 'f) CamlinternalFormatBasics.format6
type ('a, 'b, 'c, 'd) format4 = ('a, 'b, 'c, 'c, 'c, 'd) format6
type ('a, 'b, 'c) format = ('a, 'b, 'c, 'c) format4

Well it turns out there is a way to label type parameters and we are about to show you how!

Orthogonal features

One of the strength of the OCaml language is how separate orthogonal features tend to combine predictably.

It turns out OCaml’s type system has some orthogonal features that, taken together, let you label your type parameters.

Type constructors with type parameters: Type constructors allow to parametrise a whole family of types over some other types. For example, the Stdlib.Result module defines a type:
```
type ('a, 'e) t = Ok of 'a | Error of 'e
```
We call 'a and 'e the type parameters and t the type constructor because, given actual types for the parameters (say int and string) the application (int, string) t construct an actual type.

Note that the parameter name chosen to represent the error type uses the mnemonic 'e. However, when you encounter an instance such as (int, string) t, there are no indication which parameter is which. (The Result.t type is common enough through the OCaml ecosystem that this is not generally a problem; we are just setting up a small manageable example.)
Object types: Types which describe objects. These type mentions the publicly available methods of an object. Importantly for our purpose, they mention those by names and are equivalent regardless of the order they appear in.
```
type o = < get_x: int; get_y: int >
```
Type parameter constraints: Narrows down the possible instantiations of a type parameter. This is a rarely used feature but it is handy on occasions (e.g., when passing a module that is monomorphic through and through to a functor which expects one with polymorphism).
```
type 'a t = 'a list
    constraint 'a = int
```

Now putting all three features together, we can define labelled type parameters:

type 'p res = ('a, 'e) Result.t
  constraint 'p = < ok: 'a; error: 'e >

This is a bit circumvoluted, but essentially the type constructor res is a one-parameter alias for the two-parameter type constructor Result.t. And the type parameter of res is constrained to be an object type with two methods. The method names serve as our parameter labels:

let catch_exceptions
  : (unit -> 'a) -> < ok: 'a; error: string > res
  = fun f ->
  match f () with
  | v -> Ok v
  | exc -> Error (Printexc.to_string exc)

A real-world use-case

The example above is somewhat artificial: the type constructor Result.t has only two parameters and is widespread in the OCaml ecosystem. But the idea can be used for real-world use-cases. In fact it is!

In the Octez Tezos suite, one of the type constructor has six parameters. The type constructor is for RPC services and the parameters correspond to:

the type of allowed HTTP methods,
the type of parameters in the URL (think /block/<level>/operations),
the type of parameters in the URL but differently this time because of reasons irrelevant to the blog post at hand,
the type of parameters in the query section of the URL (think /version?format=<format>),
the type of parameters in the body of the request, and
the type of the returned value.

So roughly, there is a type

type ('meth, 'prefix, 'params, 'query, 'input, 'output) service = …

The details are not too important for this blog post; the important part is that this number of type parameters is cumbersome. To make the code more readable (not more concise, but more readable), we introduce a type alias using the labelled type parameter technique above:

type 'rpc service =
  ('meth, 'prefix, 'params, 'query, 'input, 'output) Tezos_rpc.Service.service
  constraint
    'rpc =
    < meth : 'meth
    ; prefix : 'prefix
    ; params : 'params
    ; query : 'query
    ; input : 'input
    ; output : 'output >

With this alias in place we use concrete types based on labels rather than position:

let post_commitment :
    < meth : [`POST]
    ; input : Cryptobox.slot
    ; output : Cryptobox.commitment
    ; prefix : unit
    ; params : unit
    ; query : unit >
    service =
  …

Without an alias

The combination of feature presented above only works as an alias of an existing type constructor with unlabelled parameters. This is the actual use-case we had in the Octez project because the service type comes from an external library.

But you can eschew the alias using GADTs. Or rather GADT syntax. For example:

type _ either =
  | Left : 'a -> <left: 'a; right: 'b> either
  | Right : 'b -> <left: 'a; right: 'b> either

The importance of orthogonal features

It could be tempting to suggest that labelled type parameters should be added to OCaml as a native feature. This could help with the syntax, with the compiler error messages, and in a few other ways. However, adding such a feature to the language increases the maintenance cost of the compiler: the feature needs to be added, tested, documented, and maintained through releases. It requires time. Time better spent adding features which are unavailable, even by combining existing features.

OCaml’s strength is not measured as the sum of its features but as ways in which these features combine together.