Why does value restriction not apply to the empty list ?

[Antoine Delignat-Lavaud <antoine.delignat-lavaud@dptinfo.ens-cachan.fr>]

[-- Attachment #1: Type: text/plain, Size: 1439 bytes --]

Dear caml experts,

While completing a project for my undergrad programming course, I have 
tumbled on a behavior in ocaml (my version is 3.10) that I don't quite 
understand.

We are required to write a polymorphic Hindley-Milner type inferer in 
Ocaml for a dialect of ML with references and lists.

I chose to solve the problem of polymorphic references by adding value 
restriction* to my inferer, using ocaml to check my results.

Not knowing whether the empty list should be considered a value or an 
expression, I copied Ocaml's behavior and made it a value.

As a result, my inferer gave the following expression the integer type :
let el = [] in if hd el then 1 else hd el ;;
which is the expected result since el has polymorphic type 'a list
but does not look right because it is used as both a bool list and an 
int list.

In Ocaml, the program
let el = [] in if List.length el > 0 then (List.hd el)+(int_of_string 
(List.hd el)) else 0 ;;
yields not type error and returns 0 despite the use of el as both an int 
list and a string list.

Thus, I am wondering why does value restriction not apply to the empty 
list in Ocaml. I don't think it's possible to do a cast with the empty 
list (it is empty after all) but I don't see any benefit in doing so.

Thanks for any tip.
With regards,
Antoine Delignat-Lavaud


* see "A syntatic approach to type soundness", A. Wright, 1992
  or "Relaxing the value restriction", J. Garrigue

[-- Attachment #2: antoine_delignat-lavaud.vcf --]
[-- Type: text/x-vcard, Size: 274 bytes --]

begin:vcard
fn:Antoine Delignat-Lavaud
n:Delignat-Lavaud;Antoine
org;quoted-printable:ENS Cachan;=C3=89l=C3=A8ve au d=C3=A9partement d'informatique
adr;dom:;;M310;Cachan
email;internet:antoine.delignat-lavaud@dptinfo.ens-cachan.fr
tel;cell:0608401862
version:2.1
end:vcard