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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id A2B70BBC1 for ; Wed, 13 Feb 2008 15:18:37 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAACOLskfAXQImh2dsb2JhbACQPQEBAQgKKYEVm0c X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="22584138" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 15:18:37 +0100 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1DEIam9024925 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 13 Feb 2008 15:18:37 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAOaKskeACH+RjGdsb2JhbACQPQEBAQgEBgkGGoEVm0g X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="8026705" Received: from server-nat-2.cs.umd.edu (HELO bacon.cs.umd.edu) ([128.8.127.145]) by mail1-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 15:18:36 +0100 Received: from [172.16.3.131] (gala.cs.umd.edu [172.16.3.131]) (authenticated bits=0) by bacon.cs.umd.edu (8.13.1/8.12.5) with ESMTP id m1DEIMv1008570 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NO) for ; Wed, 13 Feb 2008 09:18:23 -0500 Mime-Version: 1.0 (Apple Message framework v753) In-Reply-To: <4a051d930802130615l1b127f49md6e4f1c055de9238@mail.gmail.com> 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> <20080213.170018.179955875.garrigue@math.nagoya-u.ac.jp> <4a051d930802130615l1b127f49md6e4f1c055de9238@mail.gmail.com> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <80FA660E-FFEF-4499-A1B5-BAA72657E08E@cs.umd.edu> Content-Transfer-Encoding: 7bit From: Michael Hicks Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Date: Wed, 13 Feb 2008 09:18:23 -0500 To: caml-list@inria.fr X-Mailer: Apple Mail (2.753) X-CSD-MailScanner-Information: Please email staff@cs.umd.edu for more information X-CSD-MailScanner: Found to be clean X-CSD-MailScanner-SpamCheck: not spam, SpamAssassin (not cached, score=-4.399, required 5, autolearn=not spam, ALL_TRUSTED -1.80, BAYES_00 -2.60) X-CSD-MailScanner-From: mwh@cs.umd.edu X-Miltered: at discorde with ID 47B2FC3C.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 -mike:01 ocaml:01 existential:01 semantics:01 existential:01 andrej:01 andrej:01 ocaml:01 compiler:01 formalized:01 compiler:01 formalized:01 variants:01 xavier's:01 Is this something that the Jane Street people would be interested in supporting for a summer project? That might be a way to get some academics involved ... -Mike On Feb 13, 2008, at 9:15 AM, Christopher L Conway wrote: > I think the lack of a formal (or, let's say, rigorous) full-language > specification is a serious liability for OCaml. The manual is > instructive primarily by example---it doesn't give much intuition > about tricky corner cases and there are some advanced features that it > doesn't mention at all. For instance, the availability of existential > types can be inferred from a grammar production in Section 6.4 (if you > know what you are looking for), but the semantics of an existential > type are not described even superficially! > > It's understandable that nobody has found the time to do this, because > it's quite a lot of thankless work. Perhaps a way that the community > could contribute is by producing a richer specification? (I don't mean > a standardization effort and all that that implies. I mean a rigorous > effort to document the existing implementation.) > > Chris > > On Feb 13, 2008 3:00 AM, Jacques Garrigue u.ac.jp> wrote: >> 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 >> >> >> _______________________________________________ >> Caml-list mailing list. Subscription management: >> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list >> Archives: http://caml.inria.fr >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> Bug reports: http://caml.inria.fr/bin/caml-bugs >> >> > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs