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.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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 3FE31BC6B for ; Wed, 13 Feb 2008 09:00:39 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANYxskfAXQImh2dsb2JhbACQPAEBAQgKKZw/ X-IronPort-AV: E=Sophos;i="4.25,344,1199660400"; d="scan'208";a="7255054" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 09:00:39 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1D80UJ6008616 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 13 Feb 2008 09:00:38 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAIsyskeFBoIFh2dsb2JhbACQPAEBAQgKKZw/ X-IronPort-AV: E=Sophos;i="4.25,344,1199660400"; d="scan'208";a="9127082" Received: from rabbit.math.nagoya-u.ac.jp ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 09:00:29 +0100 Received: from localhost (millas [172.16.30.29]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id m1D80JG3029092; Wed, 13 Feb 2008 17:00:19 +0900 (JST) Date: Wed, 13 Feb 2008 17:00:18 +0900 (JST) Message-Id: <20080213.170018.179955875.garrigue@math.nagoya-u.ac.jp> To: Andrej.Bauer@andrej.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants From: Jacques Garrigue In-Reply-To: <47B17667.2090907@fmf.uni-lj.si> References: <18352.43565.401296.820373@nyc-qws-r03.delacy.com> <20080212.132225.27792058.garrigue@math.nagoya-u.ac.jp> <47B17667.2090907@fmf.uni-lj.si> X-Mailer: Mew version 4.0.69 on Emacs 22.0.50 / 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 47B2A39E.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 andrej:01 andrej:01 ocaml:01 compiler:01 ocaml:01 formalized:01 compiler:01 formalized:01 variants:01 xavier's:01 didier:01 vouillon:01 furuse:01 weis:01 From: Andrej Bauer > Out of curiosity, is there a document describing the current ocaml > typing system, other than the compiler source code? > > More generally, what level of formal specification and verification does > ocaml reach? None, well commented code, a fragment of the language is > formalized, someone's PhD described the compiler, there is an official > document describing the compiler, God gave Xavier the type system on Mt > Blanc, or what? Most of the type system is formalized, but there is no single place to look at. Caml Special Light (ocaml minus objects and variants) was mostly based on Xavier's work, so you can look at his papers for that part (and more recent extensions of the module system). Objects were added by Didier Remy and Jerome Vouillon, and Jerome's thesis is a good source for this. I worked on labels (with Jun Furuse) and polymorphic variants, so you may look at my papers for those. Private types are by Pierre Weis, and I suppose he wrote something on them too. And this list is not exhaustive. Of course all these papers consider each feature independently, and are not always up to date with the current ocaml implementation, but if the behaviour does not follow them, there is a high probability that this is a bug. Note also that some parts have no published formal specification. For instance, subtyping coercions, or variance inference. The intended behaviour is relatively clear though. Jacques Garrigue