From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 75E30BC84 for ; Tue, 26 Apr 2005 15:19:09 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j3QDJ8iR004780 for ; Tue, 26 Apr 2005 15:19:09 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA25226 for ; Tue, 26 Apr 2005 15:19:08 +0200 (MET DST) Received: from copper.three-tuns.net (copper.three-tuns.net [193.201.200.235]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j3QDJ8qN004771 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Tue, 26 Apr 2005 15:19:08 +0200 Received: from mark by copper.three-tuns.net with local (Exim 4.50) id 1DQPxz-0002zM-Sp for caml-list@inria.fr; Tue, 26 Apr 2005 14:19:07 +0100 Date: Tue, 26 Apr 2005 14:19:07 +0100 From: Mark Shinwell To: caml-list@inria.fr Subject: Re: [Caml-list] Type inference question Message-ID: <20050426131907.GA10841@three-tuns.net> References: <17006.11606.297786.728905@gargle.gargle.HOWL> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <17006.11606.297786.728905@gargle.gargle.HOWL> User-Agent: Mutt/1.5.9i Sender: Mark Shinwell X-Miltered: at concorde with ID 426E3FCD.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 426E3FCC.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; shinwell:01 shinwell:01 caml-list:01 inference:01 filliatre:01 myfun:01 stdin:01 myfun:01 stdin:01 forall:01 instanciated:01 non-trivial:01 sml:01 nonexpansive:01 mutable:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: 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