Type inference question
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Mark Shinwell <Mark.Shinwell@c...> 
Subject:  Re: [Camllist] Type inference question 
On Tue, Apr 26, 2005 at 02:00:22PM +0200, JeanChristophe 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 (nontrivial) 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