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=1.1 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id BB409BBC1 for ; Wed, 13 Feb 2008 15:15:49 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAOaKskfAXQInh2dsb2JhbACQPQEBAQgKKYEVlSCGKA X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="8026592" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 15:15:49 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1DEFjQs017165 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 13 Feb 2008 15:15:49 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAOaKskdIDvbxbGdsb2JhbACQMA0LBAMKAQkRBYEXlSCGKA X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="7269878" Received: from ag-out-0708.google.com ([72.14.246.241]) by mail2-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 15:15:48 +0100 Received: by ag-out-0708.google.com with SMTP id 9so14738018agd.9 for ; Wed, 13 Feb 2008 06:15:47 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; bh=eougAN3a8wJ9XvarTBhKgwj+IPXhR2JAcM9xKL8u1gs=; b=DfZYbvlMd/IsyaAsxjUVr/I9/CMgLzZoPTdqWZJKPB698LJhsG5J3U6rXw6wvOyW6CK9JJ67ctkTgvV5WNuVYWZqVujIhkvaXmZmxkqOOrghjWuxg82pp6IzZV8NXnE3rvI6hboQ6EJIKGOTLTpbAFVt9RKh03mSkIcDihAafoU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=I+Oj9nOTt3LoVn/OC6zrP/DDudSkndaCLd/3uhq2G/+vkI7kA2ehg63o1JU1Qr301FyWqPZuVM16SSyTVfBrGy8BGZUMrdp8xzf9fFSOb4sWm6/+4b3NujVqx9CRRSB6KG0DvVO/El5XCcu5yciZyw9tIvgb4O7BdGPJx1zRtI4= Received: by 10.142.77.11 with SMTP id z11mr2147947wfa.23.1202912146742; Wed, 13 Feb 2008 06:15:46 -0800 (PST) Received: by 10.142.148.14 with HTTP; Wed, 13 Feb 2008 06:15:46 -0800 (PST) Message-ID: <4a051d930802130615l1b127f49md6e4f1c055de9238@mail.gmail.com> Date: Wed, 13 Feb 2008 09:15:46 -0500 From: "Christopher L Conway" Sender: christopherleeconway@gmail.com To: "Jacques Garrigue" Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Cc: Andrej.Bauer@andrej.com, caml-list@inria.fr In-Reply-To: <20080213.170018.179955875.garrigue@math.nagoya-u.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline 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> X-Google-Sender-Auth: 25476f0c5283926a X-Miltered: at concorde with ID 47B2FB91.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants: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 didier:01 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 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 > >