[Caml-list] Why does value restriction not apply to the empty list ?
Antoine Delignat-Lavaud
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
Richard Jones
> 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
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
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:
>
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.
>
>
_______________________________________________
Antoine Delignat-Lavaud
> 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
Xavier Leroy
> 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