Re : Weak types ?

Re : Weak types ?

[Moreau]

Simon Helsen had given an explication about weak types and the reason their
existence, but there is still something i can't understand : if we do :

let toto y =
 let id x = x in
id id y ;;

this will be of type 'a ->'a
What is the difference with this :

let toto = let id x = x in id id ;;

I thought caml will understand that there is no difference !

why does caml make this difference ?

Re: Re : Weak types ?

[Simon Helsen]

> let toto y =
>  let id x = x in
> id id y ;;
> 
> this will be of type 'a ->'a
> What is the difference with this :
> 
> let toto = let id x = x in id id ;;
> 
> I thought caml will understand that there is no difference !
> 
> why does caml make this difference ?

Eta-expansion (what you're doing in the first example) indeed solves the
this common degration of polymorphic values to pseudo poly's. The
fundamental reason being the syntactic approach of value polymorhism.  The
first example is just syntactic sugar for "let toto = function y -> let id
x = x in id id y" So, toto is defined as a lambda, which is non-expansive
(and this is obvious since this type of declaration can never do something
"wrong" in the sence of polymorphic references, the actual reason value
polymorphism). However, in the 2nd example, the declaration is an
*application* (which of course results in a function, but that's
syntactically not apparent) Hence, the resulting poly value has to degrade
(to avoid potential problems with polymorphic references) 

Note that the 2nd example is again invalid Standard ML and there we rely
on eta-expansion to write something like that at all...

Hope this helps,

Simon

PS: I know people on this list are Ocaml users, but it might be worth to
look at pages 321-326 (section 8.3) of the reference below. It contains a
fairly good explanation of the problem with poly-references and value
polymorphism. It also gives a brief description of the history of this
problem:

"ML for the working programmer -2nd edition", L.C.Paulson, 1996, Cambridge
University Press

Re: Re : Weak types ?

[Pascal Cuoq]

> let toto y =
>  let id x = x in
> id id y ;;
> 
> this will be of type 'a ->'a
> What is the difference with this :
> 
> let toto = let id x = x in id id ;;
> 
> I thought caml will understand that there is no difference !
> 
> why does caml make this difference ?

the same examples, rewritten:

let id = fun x -> x ;;

let toto = fun y -> id id y ;;

caml: ha, I know the answer to this one : toto is a function.
The evaluation of "fun y -> anything" can not create references,
so type variables can safely be generalized.

let toto = id id ;;

caml: hmmm, I wonder what this toto may be... It is the result
of an application, and I don't know whether I am qualified to
look deeper into the code to check about that.  It might be
anything, I'd better not generalize variables.

About this algorithm, you can think of Caml as of 
Winnie-the-Pooh : it can answer difficult questions in the 
particular cases where the answer is obvious (ie, syntactic). 
Otherwise it doesn't know.

Pascal