From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr 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 47C38BB83 for ; Thu, 14 Sep 2006 02:24:16 +0200 (CEST) Received: from rabbit.math.nagoya-u.ac.jp (rabbit.math.nagoya-u.ac.jp [133.6.130.5]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k8E0OE6l020650 for ; Thu, 14 Sep 2006 02:24:15 +0200 Received: from localhost (moose-172 [172.16.254.3]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id k8E0OATj016678; Thu, 14 Sep 2006 09:24:10 +0900 (JST) Date: Thu, 14 Sep 2006 09:24:10 +0900 (JST) Message-Id: <20060914.092410.105434224.garrigue@math.nagoya-u.ac.jp> To: tom.primozic@gmail.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] Type system infering 'a and '_a From: Jacques Garrigue In-Reply-To: References: X-Mailer: Mew version 4.2 on Emacs 21.3 / 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 4508A12E.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; val:01 mutable:01 generalizing:01 mutable:01 type-checker:01 polymorphism:01 val:01 polymorphic:01 workaround:01 workaround:01 caml-list:01 immutable:01 variables:02 variables:02 covariant:02 From: Tom > But now... > > type ('a, 'b) t5 = > Empty_a5 of 'a option ref > | Empty_b5 of 'b option ref > | Full5 of 'a * 'b > > # let a5 = Empty_a5 (ref None);; > val a5 : ('_a, '_b) t5 = Empty_a5 {contents = None} > > Stupid. Value a5 should be polymorphic in 'b! The main role of a type system is not to be smart, just to be correct :-) So the above sentence should use "could", not "should". Let's just explain why you get this result. The decision on how to generalize is made at the level of the let. If the right hand side contains mutable values creations and/or function applications, the generalization is made in "safe" mode, generalizing only covariant type variables in the result type. This "safe" generalization is done without looking at the definition itself, so it doesn't know what caused the switch to safe mode. One can always imagine more clever approaches, like memorizing variables that cannot be generalized just where the mutable value is created, rather than decide on a whole-expression basis. In some cases this would give better types. But this also adds complexity to the type-checker, which still should be able to generalize this variable if it is covariant in the final type. And complexity can be the enemy of correctness, so this is not done currently. Do you have a concrete example where the above polymorphism is required, and there is no workaround? In general there is an (easy) workaround: separate definition of mutable parts from immutable ones. # let r = ref None;; val r : '_a option ref = {contents = None} # let a5' = Empty_a5 r;; val a5' : ('_a, 'b) t5 = Empty_a5 {contents = None} Jacques Garrigue