Here's a little trick that I find useful when I get a type error due to a function that I believe is polymorphic, but isn't due to some bug. For example, suppose I had a function

`f`

that I believed was of type `'a list -> 'a list`

, but really wasn't.

let f x = 13 :: x (* suspend disbelief -- pretend f is large and complex *) let l = f ["foo"]

If I feed this to OCaml, I get an error message at the point `f`

is applied saying:

This expression has type string but is here used with type int

I would like to find out what the error in `f`

is that makes it not polymorphic. When I first came to OCaml from SML, I was surprised to find the following did not work.

let f (x : 'a list) = 13 :: x let l = f ["foo"]

In SML, type variables in expressions are universally quantified (at a point determined by some complex rules), while in OCaml they are not. So, while SML would reject the definition of `f`

, OCaml happily unifies `a`

with `int`

and continues.

In OCaml, one can get universally quantified type variables by using the signature language.

include (struct let f x = 13 :: x end : sig val f : 'a list -> 'a list end) let l = f ["foo"]

This fails with a more helpful error message.

Signature mismatch: Modules do not match: sig val f : int list -> int list end is not included in sig val f : 'a list -> 'a list end Values do not match: val f : int list -> int list is not included in val f : 'a list -> 'a list

However, it's a lot of syntax to use the signature language, and can be difficult if the function you want is not at the top level. Furthermore, you may not want to write out the full type -- perhaps you only want to add enough of a constraint to catch the error. In SML, I just had to write the constraint on `x`

and I was done. Fortunately, one can approximate the SML solution in OCaml by using a new type that has no values.

type z let f (x : z list) = 13 :: x

This fails with an error message at the use of `x`

that is quite helpful.

This expression has type z list but is here used with type int list

If `f`

actually were polymorphic, then instantiating the polymorphism with a new type should succeed, and I would get an error later in the code at a use of `f`

. So, using this trick I can now focus on `f`

until I fix all its type errors, at which point I can remove the constraint and `type z`

.

That is very slick, and as a bonus reminds me of the intro rule for \forall:

[z / 'a] A true

——————– for fresh parameter z

\forall ‘a. A true

The lack of universally quantified variable is indeed sometimes frustrating. LexiFi’s version of OCaml has an extension

let type t in e

The expression e is typed with t being an abstract type that cannot escape to the environment. This type is then replaced by a fresh type variable in the resulting type. Since the construction does not break the value restriction (“let type” is non-expansive), one can write things like:

let f =

let type t in

fun (x : t) -> ….

to ensure some degree of polymorphism.

The construction is also useful because the type t can be used in local module. For instance, one can define in a function a local exception whose argument’s type is one of the type variables the function is polymorphic upon (this gives another solution to your “universal type” post).

This looks like a rather useful extension. Have you made any attempt to try to get it accepted upstream?

I’ve mentioned this work to caml-devel. The patch is really small and local. The feedback is not negative, but I’ve no indication that it will be considered for inclusion in upstream. We also have other useful extensions that are simple enough: a local open statement, and first-class packaged modules.

I know what local open does. What do you mean by first-class packaged modules?

Ask Markus

The idea is to turn modules (structures or functors) into values so that they can be manipulated more dynamically (passed to function, stored into data structures). This is a very convenient way to encode existential types (they can also be encoded using first-class polymorphism, a.k.a polymorphic methods, but this is less direct).

If ME is a module expression and S is a module type path, we can write the expression(module ME : S) , whose type is (module S) . To open such a packaged module, we have the expression let (module M : S) = … in … .

Here is an example:

module type S = sig type t val x : t val f : t -> t end

let s0 =

let module M = struct type t = int let x = 0 let f = succ end in

(module M : S)

let incr s =

let (module M : S) = s in

let module N = struct

include M

let x = f x

end in

(module N : S)

We also support parametrized packaged module types (module S with type t = … and type s = … …), so that we

can write:

let create =

let type s in

fun x f ->

let module M = struct type t = s let x = x let f = f end in

(module M : S with type t = s)

whose type is‘a -> (‘a -> ‘a) -> (module S with type t = ‘a) .

This feature (local introduction of an abstract type, then replaced by a type variable) has been accepted upstream. The official OCaml syntax will be:

fun (type t) -> e

instead of:

let type t in e

The construction is not a real abstraction (the evaluation of e is not suspended), but it is generally used together with real abstraction, as in:

let f (type t) (x : t) = …