From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id D5B36BC57 for ; Sat, 15 May 2010 02:54:50 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiIGAIaN7UuFBoIF/2dsb2JhbACSBYxxsC6NaAEEhRCDQg X-IronPort-AV: E=Sophos;i="4.53,234,1272837600"; d="scan'208";a="51190965" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 15 May 2010 02:54:49 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 0F2F5B633; Sat, 15 May 2010 09:54:47 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172 [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B797688AD; Sat, 15 May 2010 09:54:46 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= date:message-id:to:cc:subject:from:in-reply-to:references :mime-version:content-type:content-transfer-encoding; s=alpha; bh=xKBaBouC6iaT7qoEcjeac0QBfy8=; b=IC5nSOH/VSx0Z7GK68nKf+Y+CoXA Z16fMDtPw1asR+P9GSSSd9wH4tbXxA+AR3X0NdwUKzm39/uFF40yYD1OYg7UHoVJ yJ31qyZ6BBDgAO7v2+FPCE5Texj+1kz3o83TDodLCYtTY+2VDaMz2BWjE6PMjVK7 R4WhpYpRWn0aRQo= DomainKey-Signature: a=rsa-sha1; h=Received:Date:Message-Id:To:Cc:Subject:From:In-Reply-To:References:X-Mailer:Mime-Version:Content-Type:Content-Transfer-Encoding; b=u1wyM0mdaiRbKSyGkn7eNs1YUfAgiNnAwJui6kbvjgCAABXI2ud/Q9sI59TRgK88bCZ9cLbu1nHrctr8l9qZwh2VnZ3ekSS4dfHZregeM2Z2ZpqIX3U7OzErpCytukLOpM34mJ5SBzLe2AshqzOHwzHXeJ1TLYXdSsW5kiBg/rE=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from localhost (bsdserver02 [172.16.249.2]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 92F358894; Sat, 15 May 2010 09:54:46 +0900 (JST) Date: Sat, 15 May 2010 09:54:45 +0900 (JST) Message-Id: <20100515.095445.134122748.garrigue@math.nagoya-u.ac.jp> To: philippe.veber@googlemail.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] Closed variants, type constraints and module signature From: Jacques Garrigue In-Reply-To: References: <20100515.004940.200940107.garrigue@math.nagoya-u.ac.jp> X-Mailer: Mew version 6.3 on Emacs 22.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; variants:01 val:01 subtype:01 sig:01 val:01 struct:01 sig:01 polymorphic:01 beginners:01 incompatible:01 caml-list:01 precisely:01 constraint:01 constraint:01 variant:02 From: Philippe Veber > 2010/5/14 Jacques Garrigue > >> From: Philippe Veber >> >> > I'd like to define a type with a variable that is constrained to accept >> only >> > polymorphic variant types included in a given set of tags. That is how I >> > believed one should do : ... >> > Does anyone know why the definition of module I is rejected ? And if this >> is >> > the intended behavior, why does the following work ? >> > >> > # let v : 'a t = `a >> > ;; >> > val v : [< `a | `b > `a ] t = `a >> >> But it doesn't really work! >> More precisely, the type [< `a | `b > `a ] t is an instance of 'a t, >> not 'a t itself, an a module interface should give a type at most as >> general as the implementation. >> > > Right, I understand now there are two different mechanisms at hand here : in > the module case, the type annotation for v is a specification, in the let > binding case, it is a constraint. Seems like my question was better suited > to beginners list ! Just to be sure : module I is rejected because v should > have type 'a t for all 'a satisfying the constraint 'a = [< `a | `b ], that > contain in particular [ `b ], which is incompatible with the type of v. Is > that correct ? Yes, this is exactly the point I was trying to make. But it was a good idea to post it here: this is a rather technical point, I don't read the beginner-list usually, and your explanation is probably better than mine. >> In your case, you should simply write >> >> type t = [`a | `b] >> >> since you don't know what v may be. >> > > If i absolutely wanted to forbid other tags than `a and `b, while keeping > the possibility to manage subtype hierarchies, maybe I could also change the > code this way : > > type u = [`a | `b] > type 'a t = 'a constraint 'a = [< u ] > > module type S = sig > val v : u t > val f : 'a t -> [`a] t > end > > module I : S = struct > let v = `a > let f _ = v > end > > At least now the interpreter doesn't complain. Many thanks ! This indeed works, but I'm not sure of why you insist on defining a constrained type. What is wrong with writing directly the following? module type S = sig val v : u val f : [< u] -> [`a] end Constrained types have their uses, but I find them often confusing as the type variable you write is not really a type variable. Question of taste. Jacques Garrigue