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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id BFB97BBAF for ; Mon, 17 May 2010 16:31:54 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am0FAIDw8EuFBoIF/2dsb2JhbACRf4xyrxSNewEEhRCDQg X-IronPort-AV: E=Sophos;i="4.53,247,1272837600"; d="scan'208";a="59497833" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 17 May 2010 16:31:53 +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 BB2A6B685; Mon, 17 May 2010 23:31:51 +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 7823788B0; Mon, 17 May 2010 23:31:51 +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=kOHl0JHYhkWS3kA3Pc5q25bktAM=; b=tCsQMDMSlU+o4VZ/lYiWeyN/tlrZ /kg0CvCxZMw4eI1whsaqAn8WIs+5cbIxWIkZB6fmK8VcOCxVhxmCCwXppVaReACQ Il3lTWBtN6k8qAq5Xw50CR9Cx9XMSyNx3GVQQrerdGwfVejPBZTTi8XL4tVl4176 M61sO6p1C74IHzE= 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=XOzlEoGV+cnL8sU4Klskrd2lNUjrJyK4tYuEcU3Dkl9QJGnF9aCWRWgCFNvuOP4iQp38YUvApCuTZfyCGKySi2riDkgVyukRa8cv6myyn9fYrmVDRKgaDy/XD8AtM1dxF50Kkmr0cluU5hi0TN555wHRgDpiCKDdRnUjdelBUx4=; 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 503A288AD; Mon, 17 May 2010 23:31:51 +0900 (JST) Date: Mon, 17 May 2010 23:31:46 +0900 (JST) Message-Id: <20100517.233146.139556665.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.095445.134122748.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 notation:01 variants:01 val:01 val:01 polymorphic:01 polymorphic:01 caml-list:01 constraint:01 constraint:01 int:01 int:01 variant:02 finite:02 defined:02 From: Philippe Veber >> Constrained types have their uses, > > which are, in brief ? Now I can't see a typical use for closed polymorphic > variant types (I mean types of the form 'a t constraint 'a = [< ... ]) A typical use would be for objects, particularly when representing virtual types (see the advanced part of the tutorial, in the reference manual). Another application is to use a record notation for type variables: type 'r t = .... constraint 'r = < env:'env; loc:'loc; typ:'typ; .. > This way you can share multiple type parameters at once, and even allow transparent addition of new parameters. This was not the original goal of constraints, but I find it handy. I have no immediate example with polymorphic variants, but your arguments about scalability are valid: in some cases, constraints allow more compact types. But at a cost. >> but I find them often confusing as >> the type variable you write is not really a type variable. >> > why isn't it the case ? Aren't they simply type variables restricted to a > finite number of types ? Yes they are constrained type variables. But the problem is that the constraint is left implicit. For instance, if somewhere you have defined type 'a t constraint 'a = [< `a | `b] and inside an interface you write val f : 'a t -> int the real meaning is val f : [< `a | `b] t -> int I.e., you are hiding something. This is not the same thing as type abbreviations, because constraints are applied from the outside, while abbreviations just have to be expanded. Jacques Garrigue