Why does value restriction not apply to the empty list ?

Why does value restriction not apply to the empty list ?

[Antoine Delignat-Lavaud]

[-- 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

Re: [Caml-list] Why does value restriction not apply to the empty list ?

[Richard Jones]

On Sat, Jan 10, 2009 at 12:34:22PM +0100, Antoine Delignat-Lavaud wrote:
> 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.

It's a strange one ... when the if statement appears as a toplevel
statement, OCaml infers the type 'a list for the list:

# let el = [] ;;
val el : 'a list = []
# if List.length el > 0 then (List.hd el)+(int_of_string (List.hd el)) else 0;;
- : int = 0
# el ;;
- : 'a list = []

But the same if statement within a function definition causes an error:

# let f el =            
  if List.length el > 0 then (List.hd el)+(int_of_string (List.hd el)) else 0;;
                                                          ^^^^^^^^^^
This expression has type int but is here used with type string

Rich.

-- 
Richard Jones
Red Hat

Re: [Caml-list] Why does value restriction not apply to the empty list ?

[Arnaud Spiwack]

> It's a strange one ... when the if statement appears as a toplevel
> statement, OCaml infers the type 'a list for the list:
>   
It is not anyhow strange, it is how OCaml always does. It generalises 
types of variables introduced by a let (or equivalently at toplevel), 
types of other variables are not polymorphic.

In the case of list it should be fairly clear, by the way, that the 
empty list is the only one that has type 'a list for all 'a.
> # let el = [] ;;
> val el : 'a list = []
> # if List.length el > 0 then (List.hd el)+(int_of_string (List.hd el)) else 0;;
> - : int = 0
> # el ;;
> - : 'a list = []
>
> But the same if statement within a function definition causes an error:
>
> # let f el =            
>   if List.length el > 0 then (List.hd el)+(int_of_string (List.hd el)) else 0;;
>                                                           ^^^^^^^^^^
> This expression has type int but is here used with type string
>
> Rich.
>
>   

Re: [Caml-list] Why does value restriction not apply to the empty list ?

[Antoine Delignat-Lavaud]

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

blue storm a écrit :
> OCaml uses a relaxed value restriction : types in covariant-only
> positions (as the 'a in 'a list) are generalized. See paper [3] of
> http://caml.inria.fr/about/papers.en.html :
> http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf
>   
Thank you for your short but accurate explanation. I would have known, 
since I cited this paper in my query, if only I was more familiar with 
ocaml's type inferer.

Regards,
Antoine Delignat-Lavaud

[-- 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

Re: [Caml-list] Why does value restriction not apply to the empty list ?

[Xavier Leroy]

Antoine Delignat-Lavaud wrote:

> 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.

Yes, the empty list is a value, like all other constants.

> 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.

It is perfectly right.  The empty list can of course be used both as a
bool list and an int list; that's exactly what parametric polymorphism
is all about.

Richard Jones wrote:

> But the same if statement within a function definition causes an error:
>
> # let f el =            
>   if List.length el > 0 then (List.hd el)+(int_of_string (List.hd el)) else 0;;
>                                                           ^^^^^^^^^^
> This expression has type int but is here used with type string

This is Hindley-Milner polymorphism at work: only "let"-bound
variables can have polymorphic types, while function parameters are
monomorphic.

- Xavier Leroy