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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id DC708BBC1 for ; Wed, 13 Feb 2008 15:52:57 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAKeSskfAXQInh2dsb2JhbACQPQEBAQgKKYEVm0s X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="9144022" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 15:52:57 +0100 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1DEqtUA018690 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 13 Feb 2008 15:52:57 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAByTskeACH+RjGdsb2JhbACQPQEBAQgEBgkGGoEVm08 X-IronPort-AV: E=Sophos;i="4.25,346,1199660400"; d="scan'208";a="8028205" 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:52:56 +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 m1DEqaxD018110 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NO); Wed, 13 Feb 2008 09:52:36 -0500 In-Reply-To: <9d3ec8300802130635va73a8adr3cfd4f50ed7e3394@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> <80FA660E-FFEF-4499-A1B5-BAA72657E08E@cs.umd.edu> <9d3ec8300802130635va73a8adr3cfd4f50ed7e3394@mail.gmail.com> Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <8C6E5861-633E-4607-B9B7-171994F06FD7@cs.umd.edu> Cc: caml-list@inria.fr Content-Transfer-Encoding: 7bit From: Michael Hicks Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Date: Wed, 13 Feb 2008 09:52:37 -0500 To: "Till Varoquaux" 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 concorde with ID 47B30447.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 formalized:01 ocaml:01 -mike:01 afaik:01 formalizing:01 ocaml:01 -mike:01 existential:01 semantics:01 existential:01 andrej:01 andrej:01 compiler:01 formalized:01 I didn't mean to suggest that the entire language be formalized in a summer! I was implying that PL theory people (many of whose graduate students use OCaml) might have some reason to get involved with the project Chris proposed, and the Jane Street funding might be a vehicle for that via their students. There are a lot of smart graduate students that monitor this list (I have a few!). -Mike On Feb 13, 2008, at 9:35 AM, Till Varoquaux wrote: > 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/ > > _______________________________________________ > 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