Type inference question

Type inference question

[Julien Verlaguet]

I have the following function definition :

let myfun param=
   let res=Marshal.from_channel stdin [] in
     if res=param then
       res
     else res
;;

Since the type of "Pervasives.=" is "'a -> 'a -> bool",
I was expecting :

myfun : 'a -> 'a

I got instead :

myfun : 'a -> 'b

Is it normal ?

Re: [Caml-list] Type inference question

[Jean-Christophe Filliatre]

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.

It would be better if  Marshal.from_channel would be given a type that
cannot  be generalized ('_a)  but I  don't think  that the  ocaml type
system can do this.

Anyway, it is  always a good idea to use a  type constraint when using
marshalling functions, as in

	let (x : tau) = Marshal.from_channel ...

Hope this helps,
-- 
Jean-Christophe

Re: [Caml-list] Type inference question

[Mark Shinwell]

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

Re: [Caml-list] Type inference question

[Andreas Rossberg]

Mark Shinwell wrote:
> 
> 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?

Recent versions of OCaml employ a slightly relaxed variant of the value 
restriction that allows generalising of variables in covariant position, 
because that is always safe.

Cheers,

   - Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] Type inference question

[Mark Shinwell]

On Tue, Apr 26, 2005 at 03:41:18PM +0200, Andreas Rossberg wrote:
> Mark Shinwell wrote:
> >
> >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?
> 
> Recent versions of OCaml employ a slightly relaxed variant of the value 
> restriction that allows generalising of variables in covariant position, 
> because that is always safe.

Ah, yes---I had forgotten about that.  Thanks.

Mark
-- 
Mark Shinwell -- email: Mark.Shinwell@cl.cam.ac.uk
Theory and Semantics Group, University of Cambridge Computer Laboratory

Re: [Caml-list] Type inference question

[Jacques Garrigue]

From: Mark Shinwell <Mark.Shinwell@cl.cam.ac.uk>

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

Because ocaml now uses an improvement of the so-called "value restriction".
Rather than refusing to generalize any variable in expansive
expressions, it generalizes covariant ones, as they cannot be
used in an unsound way.
(See "Relaxing the value restriction" at
 http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/)

What we see here is a consequence of that for functions which
are known as typing holes: any function that returns a totally
unconstrained result (as input_value or Obj.magic) allows this result
to be generalized. Actually, for Obj.magic this is a good thing: you
sometimes want the result to be polymorphic (this is not a real
function anyway). For input_value this is subject for discussion, but
anyway this function is a glaring hole in the type system... maybe we
should have a way to explicitly require its result to be annotated
with a ground type!

Jacques Garrigue