The goal of this lecture note is to explain the origin of type errors whose error messages include a slash (i.e., the character /) that is followed by a version number.
As illustrated earlier, from Exercise 09 in Week 04 to the Food for thought about lexical scope in the mini-project about the underlying determinism of OCaml, new definitions shadow old ones:
# let x = true;;
val x : bool = true
# let t = fun () -> x;;
val t : unit -> bool = <fun>
# let x = 1;;
val x : int = 1
# t ();;
- : bool = true
#
In words:
This scenario features two successive versions of x.
A similar scenario can take place with two successive versions of a type:
# type 'a binary_tree = Leaf of 'a | Node of 'a binary_tree * 'a binary_tree;;
type 'a binary_tree = Leaf of 'a | Node of 'a binary_tree * 'a binary_tree
# let x = Leaf 10;;
val x : int binary_tree = Leaf 10
# type 'a binary_tree = Leaf of 'a | Node of 'a binary_tree * 'a * 'a binary_tree;;
type 'a binary_tree = Leaf of 'a | Node of 'a binary_tree * 'a * 'a binary_tree
# let y = Leaf 10;;
val y : int binary_tree = Leaf 10
# x = y;;
Characters 4-5:
x = y;;
^
Error: This expression has type int binary_tree/1020
but an expression was expected of type int binary_tree/1016
#
In words:
The issue is that x and y do not have the same type, even though their type has the same name (int binary_tree) and their denotation was constructed using a datatype constructor with the same name (Leaf) and with the same argument (10).
To distinguish these types that have the same name but that are not the same, OCaml internally associates “version numbers” with each name. When issuing a type-error message, OCaml renders these names together with their version number, separating them with a slash.
This situation looks convoluted, but it can easily occur when one duplicates definitions in one’s .ml file... or if one adds declarations that refer to something that is only declared later in the file, as illustrated next by Halcyon.
To consolidate his foundations, Halcyon is implementing the onion type all by himself. So he opens a file (C-x C-f Halcyon-s-onions.ml) and garnishes it as follows:
(* Halcyon's onions.ml *)
(* A miscellany of agricultural computations. *)
(* ********** *)
type onion =
| Bud
| Layer of onion;;
(* ********** *)
let end_of_file = "Halcyon-s-onions.ml";;
(* remember to put the digital signature here! *)
In words, he sets up the header and the footer of his file and declares the type of onions.
Thoughtfully, he then proceeds to implement a recursive function that counts the number of layers in any given onions:
(* Halcyon's onions.ml *)
(* A miscellany of agricultural computations. *)
(* ********** *)
type onion =
| Bud
| Layer of onion;;
(* ***** *)
let number_of_layers o =
let rec loop o =
match o with
| Bud ->
0
| Layer o' ->
succ (loop o')
in loop o;;
(* ********** *)
let end_of_file = "Halcyon-s-onions.ml";;
(* remember to put the digital signature here! *)
He then verifies his file with OCaml:
# #use "Halcyon-s-onions.ml";;
type onion = Bud | Layer of onion
val number_of_layers : onion -> int = <fun>
#
He then happily proceeds to also implement a tail-recursive version of the same function that uses an accumulator:
(* Halcyon's onions.ml *)
(* A miscellany of agricultural computations. *)
(* ********** *)
type onion =
| Bud
| Layer of onion;;
(* ***** *)
let number_of_layers o =
let rec loop o =
match o with
| Bud ->
0
| Layer o' ->
succ (loop o')
in loop o;;
(* ***** *)
let tr_number_of_layers o =
let rec loop o a =
match o with
| Bud ->
a
| Layer o' ->
loop o' (succ a)
in loop o 0;;
(* ********** *)
let end_of_file = "Halcyon-s-onions.ml";;
(* remember to put the digital signature here! *)
Again, he verifies his file with OCaml:
# #use "Halcyon-s-onions.ml";;
type onion = Bud | Layer of onion
val number_of_layers : onion -> int = <fun>
val tr_number_of_layers : onion -> int = <fun>
val end_of_file : string = "Halcyon-s-onions.ml"
#
Struck by inspiration, he then conceives a generator of random onions in order to test his code. Here is the result of his brainstorm with Pablito:
let nat_fold_left zero_case succ_case n =
let () = assert (n >= 0) in
let rec loop i a =
if i = 0
then a
else loop (pred i) (succ_case a)
in loop n zero_case;;
let generate_random_onion n =
let () = assert (n > 0) in
let number_of_layers = Random.int n
in (nat_fold_left Bud (fun o -> Layer o) number_of_layers, number_of_layers);;
Applying generate_random_onion to a positive integer returns a pair: the resulting random onion together with its random number of layers. Neat, isn’t it? Here it is at work:
# generate_random_onion 10;;
- : onion * int = (Layer Bud, 1)
# generate_random_onion 10;;
- : onion * int = (Layer (Layer (Layer (Layer (Layer (Layer (Layer Bud)))))), 7)
#
By then Pablito is up and running, so the unit-test function pretty much writes itself:
let test_number_of_layers name candidate =
let b0 = (candidate Bud = 0)
and b1 = (candidate (Layer Bud) = 1)
and b2 = (candidate (Layer (Layer Bud)) = 2)
and bn = (let (o, n) = generate_random_onion 100
in let expected_result = n
and actual_result = candidate o
in if actual_result = expected_result
then true
else let () = Printf.printf
"test_number_of_layers failed for %s with %d as result instead of the expected %n\n"
name
actual_result
expected_result
in false)
in b0 && b1 && b2 && bn;;
It says something about Pablito that he dutifully tests this unit-test function with a fake implementation, he is such a friend:
let fake_number_of_layers o =
match o with
| Bud ->
0
| Layer Bud ->
1
| Layer (Layer Bud) ->
2
| _ ->
-1;;
As Pablito said, the unit-test function sometimes succeeds and sometimes fails, it has something to do with the random integers that are generated:
# test_number_of_layers "fake_number_of_layers" fake_number_of_layers;;
- : bool = true
# test_number_of_layers "fake_number_of_layers" fake_number_of_layers;;
test_number_of_layers failed for fake_number_of_layers with -1 as result instead of the expected 6
- : bool = false
#
In any case, Halcyon’s file now starts to look pretty professional. First, it contains the unit tests, because one should write the unit tests first, and then it contains the implementations, each of them with a test:
(* Halcyon's onions.ml *)
(* A miscellany of agricultural computations. *)
(* ********** *)
let nat_fold_left zero_case succ_case n =
let () = assert (n >= 0) in
let rec loop i a =
if i = 0
then a
else loop (pred i) (succ_case a)
in loop n zero_case;;
let generate_random_onion n =
let () = assert (n > 0) in
let number_of_layers = Random.int n
in (nat_fold_left Bud (fun o -> Layer o) number_of_layers, number_of_layers);;
let test_number_of_layers name candidate =
let b0 = (candidate Bud = 0)
and b1 = (candidate (Layer Bud) = 1)
and b2 = (candidate (Layer (Layer Bud)) = 2)
and bn = (let (o, n) = generate_random_onion 100
in let expected_result = n
and actual_result = candidate o
in if actual_result = expected_result
then true
else let () = Printf.printf
"test_number_of_layers failed for %s with %d as result instead of the expected %n\n"
name
actual_result
expected_result
in false)
in b0 && b1 && b2 && bn;;
let fake_number_of_layers o =
match o with
| Bud ->
0
| Layer Bud ->
1
| Layer (Layer Bud) ->
2
| _ ->
-1;;
(*
# test_number_of_layers "fake_number_of_layers" fake_number_of_layers;;
- : bool = true
# test_number_of_layers "fake_number_of_layers" fake_number_of_layers;;
test_number_of_layers failed for fake_number_of_layers with -1 as result instead of the expected 6
- : bool = false
#
*)
(* ********** *)
type onion =
| Bud
| Layer of onion;;
(* ***** *)
let number_of_layers o =
let rec loop o =
match o with
| Bud ->
0
| Layer o' ->
succ (loop o')
in loop o;;
let () = assert (test_number_of_layers "number_of_layers" number_of_layers);;
(* ***** *)
let tr_number_of_layers o =
let rec loop o a =
match o with
| Bud ->
a
| Layer o' ->
loop o' (succ a)
in loop o 0;;
let () = assert (test_number_of_layers "tr_number_of_layers" tr_number_of_layers);;
(* ********** *)
let end_of_file = "Halcyon-s-onions.ml";;
(* remember to put the digital signature here! *)
But alas, three times alas, when Halcyon loads his file, the following error occurs:
# #use "Halcyon-s-onions.ml";;
val nat_fold_left : 'a -> ('a -> 'a) -> int -> 'a = <fun>
val generate_random_onion : int -> onion * int = <fun>
val test_number_of_layers : string -> (onion -> int) -> bool = <fun>
val fake_number_of_layers : onion -> int = <fun>
type onion = Bud | Layer of onion
val number_of_layers : onion -> int = <fun>
File "Halcyon-s-onions.ml", line 73, characters 58-74:
Error: This expression has type onion/1540 -> int
but an expression was expected of type onion/1502 -> int
Type onion/1540 is not compatible with type onion/1502
#
This error is so weird. Line 73 (M-x goto-line 73 RET) reads:
let () = assert (test_number_of_layers "number_of_layers" number_of_layers);;
which suggests that number_of_layers does not pass the unit test, which it should since Pablito interactively checked that it did.
It took Dana quite some time to explain, and to be honest her explanation about OCaml’s internal versioning of declarations doesn’t make sense. When the file is loaded, the unit-test function refers to the definition of the onion type that was declared the previous time the file was loaded. Then the onion type is declared and number_of_layers refers to this new definition. So when the test is ran, the unit-test function refers to the previous instance of the onion type and the tested function refers to its new instance, or something, which doesn’t make any sense since they have the same name: it’s the same elephant, no? Then Anton said to forget the elephant and to concentrate on the temporality of the onion as evidenced by its version number after the slash, Halcyon tried to joke his way out by suggesting that OCaml should go forth to the past, and Loki mumbled something about Marty McFly. That’s when Mimer arrived. But by then Halcyon had rebooted his laptop and re-loaded the file:
# #use "Halcyon-s-onions.ml";;
val nat_fold_left : 'a -> ('a -> 'a) -> int -> 'a = <fun>
File "Halcyon-s-onions.ml", line 17, characters 20-23:
Error: Unbound constructor Bud
#
Obviously, the definition of the onion should occur first in the file. With that fixed, the file loaded without any hiccup:
# #use "Halcyon-s-onions.ml";;
type onion = Bud | Layer of onion
val nat_fold_left : 'a -> ('a -> 'a) -> int -> 'a = <fun>
val generate_random_onion : int -> onion * int = <fun>
val test_number_of_layers : string -> (onion -> int) -> bool = <fun>
val fake_number_of_layers : onion -> int = <fun>
val number_of_layers : onion -> int = <fun>
val tr_number_of_layers : onion -> int = <fun>
val end_of_file : string = "Halcyon-s-onions.ml"
#
Not just that, but Mimer said it was a good idea to put the unit tests first, that the unit-test function was professional, and that the fake function was a nice touch because of Dijkstra. All in all, it was a pretty good day!
Halcyon: Moi, je m’occupe de mes oignons.
If a type error occurs with a slash followed by a version number, stop OCaml, restart it, and move a definition in this file so that what is defined is declared before it is used.
Explain in your own words the reasons for a type error with a slash followed by a version number, and provide a simple example of it in the form of a separate .ml file (or of several consecutive .ml files).
Hint: read the present chapter.
John Doe is a happy elephant. He is just moving in a new apartment, and notices with amusement that the previous elephant who occupied his apartment was also named John Doe: he doesn’t even need to change the name on the front door. Life goes on for a while until somehow he borrows money from a loan shark. Imagine his surprise when the delegate of another loan shark comes to get the other loan shark’s money back. This delegate flatly doesn’t buy John Doe’s explanation about not being the elephant who borrowed money from the other loan shark. (To make sure, the delegate checks both John Doe’s Social Security card and his name on the front door.) Anyhow, since that was the last warning, John Doe is killed on the spot. That’s the tragic part of this story, born from confusion.
John Doe’s body is then brought to the city morgue for elephants. A tag that reads “John Doe/142” is affixed on its back leg.
Coincidentally, another body is also brought to the morgue. A tag that reads “John Doe/143” is affixed on its back leg. (It could be the body of the previous John Doe because of yet another loan shark or it could be an ID-less body, who knows and can we please move on?)
At any rate, when the delegate of John Doe’s loan shark tries to locate him and eventually finds a body with that name at the morgue, he can plainly see that it’s not the same elephant and versioning is kind of not on his mind. That’s the confusing part of this story, born from tragedy.
Anton: So versioning is to distinguish two denotations that have the same name.Alfrothul: Right. So that the latest declaration of this name does not shadow the previous one.Dana: And aliasing is what happens when the same denotation has two names.Pablito: OK...