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=0.0 required=5.0 tests=none 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 55C08BC0A for ; Tue, 15 May 2007 11:45:26 +0200 (CEST) Received: from orion.metastack.com (no-dns-yet.demon.co.uk [80.177.38.218] (may be forged)) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l4F9jPIL002573 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Tue, 15 May 2007 11:45:26 +0200 Received: from treble (cpc2-cmbg6-0-0-cust535.cmbg.cable.ntl.com [81.107.34.24]) (authenticated bits=0) by orion.metastack.com (8.13.4/8.13.3) with ESMTP id l4F9i0rn030482 (version=TLSv1/SSLv3 cipher=RC4-MD5 bits=128 verify=NO); Tue, 15 May 2007 10:44:01 +0100 From: "David Allsopp" To: "'Jacques Garrigue'" , References: <20070514100005.459F6BC70@yquem.inria.fr><002c01c79615$e9750b30$6a7ba8c0@treble> <20070515.134054.08075760.garrigue@math.nagoya-u.ac.jp> Subject: RE: [Caml-list] Polymorphic variant difference... Date: Tue, 15 May 2007 10:45:03 +0100 Organization: MetaStack Solutions Ltd. Message-ID: <001601c796d5$b723b6c0$6a7ba8c0@treble> MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Mailer: Microsoft Office Outlook 11 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.3028 Thread-Index: AceWqx38zQwZlmiuS3+XkjinqkF1/QADt/LQ In-Reply-To: <20070515.134054.08075760.garrigue@math.nagoya-u.ac.jp> X-Miltered: at discorde with ID 46498135.004 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; elt:01 elt:01 parsing:01 failwith:01 val:01 ocamldoc:01 variants:01 subtraction:01 foo:01 mli:01 foo:01 mli:01 subtraction:01 syntax:01 syntax:01 A SQL converter I'm writing ends up with these two types: type t' = [ `CreateDB of ... | `CreateType of ... | `CreateTable of ... | `CreateFunction of ... | `CreateProcedure of ... | `CreateRole of ... | `Eof ] type t = [ `Comment of ... | `Block of ... | `Blank | t' ] Solely so that further down the code I can say: match elt with `Block block -> ... | `Comment comment -> ... | `Blank -> ... | #t' as elt -> (* specific code only relevant when elt <> `Block, `Comment or `Blank *) match elt with (* Remaining match cases not including the three checked already *) type t' is only defined for use in # matches (the actual code will translate a variant-SQL script to T-SQL and is compacting custom blocks of unparsed SQL code, comments and blank lines into a single `Block before parsing actual clauses that it understands how to translate). If I don't use #t' then, as far as I can see, I must either add redundant matches to the second match block to prevent match warnings (and so have an "Unexpected" exception or failwith "programmer is an idiot" call for these 'unreachable' match clauses) or duplicate a lot of code between the match clauses. I equally get it with certain error handling matches: e.g. (contrived again, but I'd have to send a lot of code for a real version... this comes up with error handling between read/write functions in a socket stream! ) type t' = [ `B | `C ] type t = [ `A | t' ] val f : int -> [ `Success of int | `Error of t ] exception SpecialExceptionForA exception GeneralException of int (* NB matter of personal taste: I don't consider x in this function but I know that's not everyone's view!! *) let g x = match x with `B -> 0 | `C -> 1 match f 0 with `Success int -> true | `Error `A -> raise SpecialExceptionForErrorA | `Error (#t' as x) -> raise (GeneralException(g x)) It would be, I think, clearer (especially when considering ocamldoc comments**) for the type to be: type t = [ `A | `B | `C ] ... match f 0 with `Success int -> true | `Error `A -> ... | `Error (#t minus [ `A ] as x) -> ... So, in summary, my irritation lies with the need to create extra types just for the # matches. But I am very fussy :o) Of course, this is related to a previous thread: http://tinyurl.com/yp7rvy ... for polymorphic variants, it would be inferring the subtraction of `A from the type of x automatically because of the previous match clause. David ** Furthermore, I can't even hide these redundant types in the implementation: Foo.mli type t = [ `A | `B ] Foo.ml type t' = [ `A ] type t = [ `A | t' ] Is not valid even though t is /effectively/ the same p-variant in both the .mli and .ml -----Original Message----- From: Jacques Garrigue [mailto:garrigue@math.nagoya-u.ac.jp] Sent: 15 May 2007 05:41 To: dra-news@metastack.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic variant difference... From: "David Allsopp" > > 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