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 05BFABC84 for ; Tue, 26 Apr 2005 15:54:33 +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 j3QDsWAq010882 for ; Tue, 26 Apr 2005 15:54:32 +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 PAA28110 for ; Tue, 26 Apr 2005 15:54:31 +0200 (MET DST) Received: from rabbit.math.nagoya-u.ac.jp (rabbit.math.nagoya-u.ac.jp [133.6.130.5]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j3QDsTXW010870 for ; Tue, 26 Apr 2005 15:54:31 +0200 Received: from localhost (millas [172.16.30.29]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id j3QDsCQk001593; Tue, 26 Apr 2005 22:54:12 +0900 (JST) Date: Tue, 26 Apr 2005 22:54:13 +0900 (JST) Message-Id: <20050426.225413.112628332.garrigue@math.nagoya-u.ac.jp> To: Mark.Shinwell@cl.cam.ac.uk Cc: caml-list@inria.fr Subject: Re: [Caml-list] Type inference question From: Jacques Garrigue In-Reply-To: <20050426131907.GA10841@three-tuns.net> References: <17006.11606.297786.728905@gargle.gargle.HOWL> <20050426131907.GA10841@three-tuns.net> X-Mailer: Mew version 4.0.69 on Emacs 21.3.50 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 426E4818.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 426E4815.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 inference:01 shinwell:01 shinwell:01 stdin:01 sml:01 nonexpansive:01 mutable:01 ocaml:01 ocaml:01 expansive:01 wwwfun:01 ...:98 polymorphic:01 marshal: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: From: Mark Shinwell > 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