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=1.0 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, RCVD_IN_BL_SPAMCOP_NET autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 8320FBC68 for ; Mon, 16 Oct 2006 01:38:00 +0200 (CEST) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id k9FNbwDj030843 for ; Mon, 16 Oct 2006 01:38:00 +0200 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.7/8.13.7) with ESMTP id k9FNbsir004375; Mon, 16 Oct 2006 08:37:54 +0900 (JST) Date: Mon, 16 Oct 2006 08:37:19 +0900 (JST) Message-Id: <20061016.083719.07640748.garrigue@math.nagoya-u.ac.jp> To: dbueno@gmail.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] Type error From: Jacques Garrigue In-Reply-To: <6dbd4d000610142029m92d7005v65e95f031e7eae9b@mail.gmail.com> References: <6dbd4d000610142029m92d7005v65e95f031e7eae9b@mail.gmail.com> 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 discorde with ID 4532C656.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; val:01 polymorphism:01 ocaml:01 typing:01 caml-list:01 constructor:01 functions:01 define:01 omitted:01 argument:02 variant:02 garrigue:03 garrigue:03 dependent:03 dependent:03 From: "Denis Bueno" > Interface: > ,---- > | val of_array: ?getter : ('b -> 'a) -> 'b array -> 'a t > | (** [of_array xs] returns a set containing the elements in [xs]. *) > `---- As somebody already pointed out, this interface is problematic. It asks for a function ('b -> 'a), but says that it can do without one, for any 'a and 'b. However, the only function of type ('b -> 'a) when 'a and 'b are different (which is allowed by the interface) is Obj.magic, which is clearly not what you intend. Actually, what you would want is some kind of dependent typing: * if getter is provided, then 'a and 'b may be different * if getter is omitted, then 'a and 'b must be equal, i.e. the type is ?getter:('a -> 'a) -> 'a array -> 'a t This is clearly much stronger than the polymorphism of ocaml, which requires the same type to be valid in both cases, i.e. 'a = 'b even if getter is provided. Some extensions to the type system, like GADT or dependent polymorpic variant matching, might allow something close to what you ask for, but you would still have to pass a special constructor for getter rather than omit it, so there would be no improvement. The only simple solution I see is to define two functions, one with an extra argument and one without. Jacques Garrigue