From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 95CA7BC48 for ; Thu, 31 Mar 2005 14:04:19 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j2VC4ITi009065 for ; Thu, 31 Mar 2005 14:04:18 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id OAA00017 for ; Thu, 31 Mar 2005 14:04:18 +0200 (MET DST) Received: from wproxy.gmail.com (wproxy.gmail.com [64.233.184.207]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j2VC4Hu2009062 for ; Thu, 31 Mar 2005 14:04:18 +0200 Received: by wproxy.gmail.com with SMTP id 69so509099wri for ; Thu, 31 Mar 2005 04:04:17 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:references; b=W7b2fI54t0boHKPiL6ml4kyfLH5KKhzhRYMbVWMg/E1EpVoXOC2VCXz39mixoLntoq36Wpv53RrGhSqVbGHCoCvZy98im4BM9vSckuNUMBKBvf+gHMpAyXmZMiN0wuXgQL9J67t6qP5HP4fPC/b2XSHrBbBJOM++9uBTk5H2Sgg= Received: by 10.54.65.5 with SMTP id n5mr322856wra; Thu, 31 Mar 2005 04:04:17 -0800 (PST) Received: by 10.54.2.79 with HTTP; Thu, 31 Mar 2005 04:04:17 -0800 (PST) Message-ID: <891bd33905033104045705be7a@mail.gmail.com> Date: Thu, 31 Mar 2005 07:04:17 -0500 From: Yaron Minsky Reply-To: yminsky@cs.cornell.edu To: Jacques Garrigue Subject: Re: [Caml-list] When is a function polymorphic? Cc: caml-list@inria.fr In-Reply-To: <20050331.173223.128566586.garrigue@math.nagoya-u.ac.jp> Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit References: <891bd339050330165142478f37@mail.gmail.com> <20050331.114253.48852731.garrigue@math.nagoya-u.ac.jp> <891bd33905033020045cad3ce2@mail.gmail.com> <20050331.173223.128566586.garrigue@math.nagoya-u.ac.jp> X-Miltered: at nez-perce with ID 424BE742.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 424BE741.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; yaron:01 minsky:01 yminsky:01 caml-list:01 yaron:01 minsky:01 yminsky:01 avoided:01 predictable:01 variants:01 avoiding:01 constructors:01 variants:01 type-safe:01 wrote: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=RCVD_BY_IP autolearn=disabled version=3.0.2 X-Spam-Level: On Thu, 31 Mar 2005 17:32:23 +0900 (JST), Jacques Garrigue wrote: > From: Yaron Minsky > > > Interesting. I guess this is best understood as a limitation of the > > type-checking algorithm. Does anyone know if there are any plans to > > remove this limitation? Are there fundamental reasons why it would be > > difficult to do so? > > This is not a limitation of the type checking algorithm per se. > Rather, the type checking algorithm prefers not to use > exhaustiveness information when this can be avoided, to keep it > predictable. > (Exhaustiveness is only used for polymorphic variants, but for > a deeper reason.) I guess I'm somewhat out of my depth. I don't quite understand what you mean by exhaustiveness information, and I don't see why avoiding it improves predictability. Do you have an example in mind? > Is it so difficult to make the extra constructors explicit? I'd say there are two issues. The first is that it really can be a pain for large variant types, particularly when the contents of those types are changing during development, and you don't want the function in question to depend on anything other than the particular variants being modified. The second issue is that it just seems like a violation of the principle of least surprise. The fact that this fails to compile: # function Some x -> Some (float x) | x -> x;; This expression has type int option but is here used with type float option but that this does compile: # function Some x -> Some (float x) | None as x -> x;; was quite unexpected, at least by me. That said, it's not all that bad. It just seems confusing, and since I don't see the downside of accepting both functions as type-safe, I don't understand why it's not done. y