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
.