From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q068uVZq030496 for ; Fri, 6 Jan 2012 09:56:31 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApMBAAS3Bk+LEwExe2dsb2JhbABDrQgiAQEWJgUggXIBAQEEOAIGAQE3AQ8LGC5XBogPo2uEIQGOBgeLLmOnQQ X-IronPort-AV: E=Sophos;i="4.71,467,1320620400"; d="scan'208";a="138095042" Received: from hera.mpi-sb.mpg.de ([139.19.1.49]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 06 Jan 2012 09:56:25 +0100 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=From:To:In-Reply-To:Subject: References:Message-Id:Content-Type:Content-Transfer-Encoding: Mime-Version:Date:Cc; bh=wYgNUHEqvSxnKF1/kxuBHP8XdyK2KbxKuFiyccK 6N1k=; b=YGh95LQfY51LfDFEQCKhRQKUkXJ1/ln9kpp02roN8im63IjjMTHjJnv L7WCfOddOPM2PJbsfh1kUoil8w+zp2xT3wG+jpttQZ+izuCqnrFvH9D4DJEsggbg 45wv/sl+Jfir3A8wSs4cN5Wk9ULKm/Ngj1h6Cty83T2mecxLAwVA= Received: from srv-00-125.mpi-klsb.mpg.de ([139.19.1.28]:50967 helo=newmaniac.mpi-klsb.mpg.de) by hera.mpi-sb.mpg.de (envelope-from ) with esmtp (Exim 4.69) id 1Rj5b4-0007FE-Ez; Fri, 06 Jan 2012 09:56:24 +0100 Received: from mnch-5d85d568.pool.mediaways.net ([93.133.213.104]:64309 helo=[192.168.178.31]) by newmaniac.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.72) id 1Rj5b4-0006x6-2O; Fri, 06 Jan 2012 09:56:22 +0100 From: Andreas Rossberg To: Andrej Bauer In-Reply-To: References: Message-Id: <8ED26AE5-A208-49A2-A8CD-43F22E969FF9@mpi-sws.org> Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v936) Date: Fri, 6 Jan 2012 09:56:21 +0100 Cc: caml X-Mailer: Apple Mail (2.936) Subject: Re: [Caml-list] Proposal for extensible open datatypes 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). /Andreas