From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
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 discorde.inria.fr (discorde.inria.fr [192.93.2.38])
	by yquem.inria.fr (Postfix) with ESMTP id 09D5EBC0A
	for <caml-list@yquem.inria.fr>; Tue, 15 May 2007 06:41:12 +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 l4F4f9Fk027492
	for <caml-list@yquem.inria.fr>; Tue, 15 May 2007 06:41:11 +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 l4F4f2fh029198;
	Tue, 15 May 2007 13:41:04 +0900 (JST)
Date: Tue, 15 May 2007 13:40:54 +0900 (JST)
Message-Id: <20070515.134054.08075760.garrigue@math.nagoya-u.ac.jp>
To: dra-news@metastack.com
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Polymorphic variant difference...
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <002c01c79615$e9750b30$6a7ba8c0@treble>
References: <20070514100005.459F6BC70@yquem.inria.fr>
	<002c01c79615$e9750b30$6a7ba8c0@treble>
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 464939E5.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; subtraction:01 syntax:01 syntax:01 constructors:01 camlp:01 camlp:01 coercions:01 coerced:01 polymorphic:01 polymorphic:01 syntactic:01 caml-list:01 variant:02 variant:02 defined:02 

From: "David Allsopp" <dra-news@metastack.com>

> > Given a polymorphic variant type t with a label `B how does one build
> > the type corresponding to t without the label `B.
> 
> So that you could write something like:
> 
> type t = [ `A | `B | `C ]
> 
> let f x =
>   match x with
>     `B                     -> (* x has type t *)
>   | #(t minus [ `B ]) as x -> (* x has type [ `A | `C ] *)
> 
> I end up having to write lots of tedious extra types to achieve that
> normally... I'd find a subtraction syntax very handy too.

There is no theoretical difficulty in adding this (when t is defined),
but this would mean yet more syntax...
I would be curious to see code where this becomes such a pain.
In my view, having to name this type should help clarity.

> On a similar subject, am I the only person who finds I often need to take a
> fixed polymorphic variant value and coerce it so that it can just accept
> more constructors e.g. (seriously contrived example)...
> 
> type t = [ `A | `B | `C ]
> 
> let f (x : t) =
>   match x with
>     `A -> `D
>   | _  -> (x : t :> [> t ])
> 
> Something more concise than (x : t :> [> t ]) would be nice: e.g. (x ::> t)
> But perhaps that really is a job for camlp4!

Indeed, this one is just about syntactic sugar, so camlp4 can do it.
An alternative without new syntax would be to let
  (x :> [> t]) mean (x : [< t] :> [> t]),
but this would break the invariant that coercions always work when the
coerced value is already an instance of the target type (not that
anybody uses this invariant...)

Jacques Garrigue