On Tue, Apr 26, 2005 at 02:00:22PM +0200, Jean-Christophe Filliatre wrote:
> Julien Verlaguet writes:
>  > I have the following function definition :
>  > 
>  > let myfun param=
>  >    let res=Marshal.from_channel stdin [] in
>  >      if res=param then
>  >        res
>  >      else res
>  > 
>  > I was expecting : myfun : 'a -> 'a
>  > 
>  > I got instead : myfun : 'a -> 'b
>  > 
>  > Is it normal ?
> 
> Yes.  "Marshal.from_channel stdin  []" has  type 'a  and this  type is
> generalized  in the  let/in  construct, giving  res  the type  "forall
> 'a. 'a". In the test "res = param", the type of res is instanciated on
> the type of param, but this does not affect the type of the result.

I can understand this behaviour in a case such as the following:

	let f v =
	  let r = fun x -> x in
	    if r = v then r else r

where as you say the (non-trivial) type scheme assigned to r is
instantiated multiple times, yielding ('a -> 'a) -> 'b -> 'b for f.

However, in the Marshal example above, we have

	Marshal.from_channel stdin []

in the first part of the "let".  In the SML terminology, this is not a
"nonexpansive expression"[*] (unlike "fun x -> x").  Therefore, I would
have thought that the appearance of such an expression here would
prohibit generalisation (in order to prevent possible unsoundness in the
presence of mutable state).  This is presumably not the case in OCaml:
can someone explain why?

Mark

[*] http://www.smlnj.org//doc/Conversion/types.html
-- 
Mark Shinwell -- email: Mark.Shinwell@cl.cam.ac.uk
Theory and Semantics Group, University of Cambridge Computer Laboratory