Why is there an error when I add type annotations to this local function?

Viewed 67

I defined a function id without type annotations:

# let id x = x;;
val id : 'a -> 'a = <fun>
# id 123;;
- : int = 123
# id true;;
- : bool = true

Everything is working as expected.

I defined id again, this time with type annotations:

# let id (x : 'a) : 'a = x;;
val id : 'a -> 'a = <fun>
# id 123;;
- : int = 123
# id true;;
- : bool = true

Everything is working as expected.

Then, I defined id again in a local expression without type annotations:

# let id x = x in
  let _ = id 123 in
  id true;;
- : bool = true

Everything is working as expected.

Then, I defined id again in a local expression with type annotations:

# let id (x : 'a) : 'a = x in
  let _ = id 123 in
  id true;;
Error: This expression has type bool but an expression was expected of type
         int

Surprise! There is an error!

Why does the error occur? How does the last definition differ from the first three? I don't see how the type annotations are causing the error.

1 Answers

First, it is important to note that OCaml's semantics for type variables is odd and not what you may expect. They are treated as unification variables, not necessarily polymorphic. For example, the following is totally fine, since 'a will simply be unified with int:

# let f (x : 'a) = x + 1;;
val f : int -> int = <fun>

Now, your example probably has to do with the implicit scoping rules for such type variables. I presume that Ocaml scopes them at the surrounding module-level declaration. That implies that you are actually defining a monomorphic function over some yet undetermined type 'a in the last example.

You can observe that with an example that only invokes id once, but forces 'a to be a specific type by other means:

# let id (x : 'a) = x in ((5 : 'a); id true);;
Error: This expression has type bool but an expression was expected of type
         int

You can get a similar effect without even calling id:

# let id (x : 'a) = x in ((5 : 'a); (true : 'a));;
Error: This expression has type bool but an expression was expected of type
         int
Related