From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q069OgS2031767 for ; Fri, 6 Jan 2012 10:24:42 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlQBAPS8Bk+DbwiXmWdsb2JhbABDrQkiAQEBAQEICwsHFCWBcgEBBThBEAEKGC5XBogPth+MEQSaVoxm X-IronPort-AV: E=Sophos;i="4.71,467,1320620400"; d="scan'208";a="125810100" Received: from ppsw-51.csi.cam.ac.uk ([131.111.8.151]) by mail4-smtp-sop.national.inria.fr with ESMTP; 06 Jan 2012 10:24:39 +0100 X-Cam-AntiVirus: no malware found X-Cam-SpamDetails: not scanned X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from hermes-2.csi.cam.ac.uk ([131.111.8.54]:34847) by ppsw-51.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:25) with esmtpa (EXTERNAL:lpw25) id 1Rj62Q-0002Ia-YR (Exim 4.72) (return-path ); Fri, 06 Jan 2012 09:24:38 +0000 Received: from prayer by hermes-2.csi.cam.ac.uk (hermes.cam.ac.uk) with local (PRAYER:lpw25) id 1Rj62Q-0006Jb-K8 (Exim 4.67) (return-path ); Fri, 06 Jan 2012 09:24:38 +0000 Received: from [86.22.78.1] by webmail.hermes.cam.ac.uk with HTTP (Prayer-1.3.4); 06 Jan 2012 09:24:38 +0000 Date: 06 Jan 2012 09:24:38 +0000 From: Leo P White To: Andreas Rossberg Cc: Andrej Bauer , caml Message-ID: In-Reply-To: <8ED26AE5-A208-49A2-A8CD-43F22E969FF9@mpi-sws.org> References: <8ED26AE5-A208-49A2-A8CD-43F22E969FF9@mpi-sws.org> X-Mailer: Prayer v1.3.4 Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset=ISO-8859-1 Sender: "L.P. White" Subject: Re: [Caml-list] Proposal for extensible open datatypes On Jan 6 2012, Andreas Rossberg wrote: >On Jan 6, 2012, at 07.26 h, Andrej Bauer wrote: >> I would be interested to hear what propeties of Ocaml you had to give >> up to get this interesting extension working? For example, what >> happens with checking for exhaustivness of match? Caml performs >> various optimizations in pattern matching, why are those still ok now >> that new alternatives may appear later? > >One such type is already in ML, for historical reasons it happens to >be named exn. Consequently, you don't really give up anything, your >questions already apply to the exception type. Exhaustiveness simply >requires a catch-all in all pattern matches over this type. More >difficult is irredundancy, because constructors can be aliased without >the type system tracking that (and it cannot across module >boundaries). You have to give up there. > >Generalising exn this way is an old idea, e.g. we implemented it in >Alice ML. The standard reply to requesting such an extension is that >it's not really needed, because you can already do everything using >exn (though without custom type distinctions, and minus GADTs in OCaml). Yes, it uses the same same pattern matching as exn. This means that a catch-all pattern is required for exhaustiveness, and if-then-elses are used instead of jump tables. The problem would become a bit more interesting if ordinary variant types could also be made open, thus allowing types to have both ordinary constructors and extensions, but the patch doesn't support that yet. Leo