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.0 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 26D5BBBC1 for ; Wed, 13 Feb 2008 15:35:54 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJyPskfAXQImh2dsb2JhbACQPQEBAQgKKYEVlR+GKw X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="8027510" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 15:35:53 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1DEZgj8025698 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 13 Feb 2008 15:35:53 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGuOskdIDvb3f2dsb2JhbACQPQEBCQQFCAoRBYEXlRqGLQ X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="22584835" Received: from ag-out-0708.google.com ([72.14.246.247]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 15:35:52 +0100 Received: by ag-out-0708.google.com with SMTP id 9so14776435agd.9 for ; Wed, 13 Feb 2008 06:35:51 -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:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; bh=Zz1CpCwKDq+LFZVPUNBjQbUs7bolPc6YE4A/KOHh4wI=; b=jj8p7CFNsdMtF/c20gyBNxbzk+ntxh33N+oIV8MVoKnxAtIEINopFozd5OJFNGeHXV6ABLtLnbtYyN/v90AldA2CeDfbxNvK0aLIDDh+QjL0gD0yu7NQhxs8AvAQyav3XHBkl88jD3j6dDuP0+sIwfGYadrw1/xRD/rJH7QLy/g= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=VdoMV716jnvkOLc8q34gucO16fgF7D1qqsLE582gaRR9DlAI7dGgxvAMcbpaX5OMdnsl1s6IFrx/IQSG+6bcrK+4xwFv1bVD5s75/PsraV5zpOWbYcmXuYWi9OcliB6/ZQPr0Xx+x23y2ebdhJF0sqsNf04pXr+sEUnTWu4JDAo= Received: by 10.142.141.21 with SMTP id o21mr2161723wfd.56.1202913350455; Wed, 13 Feb 2008 06:35:50 -0800 (PST) Received: by 10.142.115.3 with HTTP; Wed, 13 Feb 2008 06:35:50 -0800 (PST) Message-ID: <9d3ec8300802130635va73a8adr3cfd4f50ed7e3394@mail.gmail.com> Date: Wed, 13 Feb 2008 14:35:50 +0000 From: "Till Varoquaux" To: "Michael Hicks" Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Cc: caml-list@inria.fr In-Reply-To: <80FA660E-FFEF-4499-A1B5-BAA72657E08E@cs.umd.edu> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 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> <4a051d930802130615l1b127f49md6e4f1c055de9238@mail.gmail.com> <80FA660E-FFEF-4499-A1B5-BAA72657E08E@cs.umd.edu> X-Miltered: at discorde with ID 47B3003E.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 afaik:01 formalizing:01 ocaml:01 -mike:01 ocaml:01 existential:01 semantics:01 existential:01 andrej:01 andrej:01 compiler:01 formalized:01 compiler:01 formalized:01 First of all the views expressed in this mail are purely personnel and do not reflect my employers. AFAIK SML is the only language that has a formal semantic. ECMA script might get one soon (a reference SML interpreter). Doing a formal semantic is time consuming and quite involved, as pointed out by Peter Sewell in response to this very thread, Scott Owens has done a considerable amount of work formalizing a good part of OCaml. This is a research subject, just reading and grasping such a semantic is probably beyond the reach (that is without having to hone a fair amount of new skills) of most of us and certainly beyond mine. I would be very impressed if a student managed to write a full formal semantic in a summer. I do think considering this for a summer project is a *little* over ambitious. It would however most probably "get some academics involved" and probably get you a shiny nice PHD (that is if you do not already have one). Till On Feb 13, 2008 2:18 PM, Michael Hicks wrote: > 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 > > _______________________________________________ > 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 > -- http://till-varoquaux.blogspot.com/