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.0 required=5.0 tests=none 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 60A4FBBC1 for ; Wed, 13 Feb 2008 17:54:18 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHivskfAXQInh2dsb2JhbACQPQEBAQgKKZxY X-IronPort-AV: E=Sophos;i="4.25,347,1199660400"; d="scan'208";a="22590370" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 17:54:18 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1DGsCA8024303 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 13 Feb 2008 17:54:17 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAO+vskdDz4He/2dsb2JhbACtVQ X-IronPort-AV: E=Sophos;i="4.25,347,1199660400"; d="scan'208";a="9148733" Received: from fettunta.fettunta.org ([67.207.129.222]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 17:54:16 +0100 Received: from aquarium.takhisis.invalid (unknown [10.17.0.10]) by fettunta.fettunta.org (Postfix) with ESMTP id 7A9371818D for ; Wed, 13 Feb 2008 16:54:07 +0000 (UTC) Received: by aquarium.takhisis.invalid (Postfix, from userid 1000) id 0DCE0125AD6; Wed, 13 Feb 2008 17:53:43 +0100 (CET) Date: Wed, 13 Feb 2008 17:53:43 +0100 From: Stefano Zacchiroli To: caml-list@inria.fr Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Message-ID: <20080213165343.GA5992@takhisis.invalid> Mail-Followup-To: caml-list@inria.fr 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 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <9d3ec8300802130635va73a8adr3cfd4f50ed7e3394@mail.gmail.com> User-Agent: Mutt/1.5.17+20080114 (2008-01-14) X-Miltered: at concorde with ID 47B320B4.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; zacchiroli:01 zack:01 variants:01 afaik:01 semantics:01 ocaml:01 ocaml:01 semantics:01 afaik:01 model:01 haskell:01 haskell:01 cheers:01 zacchiroli:01 zack:01 On Wed, Feb 13, 2008 at 02:35:50PM +0000, Till Varoquaux wrote: > AFAIK SML is the only language that has a formal semantic. ECMA script > might get one soon (a reference SML interpreter). I don't think anybody asked for a formal semantics. Of course it might be something *really* useful, but for the purpose of a user manual (where with "user" I mean Random J OCaml developer) a rigorous prose would be enough. It is still something we are missing for OCaml. Just because you mentioned examples, another example is Python. It has no formal semantics AFAIK, but still the reference manual describes the data model of values the programmer can depict in her mind to understand the current interpreter status. Then, each language feature is described by giving its grammar entry in the global language grammar, and its semantics is described---with prose---in terms of modifications of such a status. (And of course we don't like such a description since we are functional programmers, but that's another issue.) I'm not that inside the Haskell world, but the Haskell report seems to be something really similar. Why should we be lacking behind such reference manuals, especially considering that the roots of our language reside in formal papers already published somewhere, is something which keeps astonishing me. Cheers. -- Stefano Zacchiroli -*- PhD in Computer Science ............... now what? zack@{upsilon.cc,cs.unibo.it,debian.org} -<%>- http://upsilon.cc/zack/ (15:56:48) Zack: e la demo dema ? /\ All one has to do is hit the (15:57:15) Bac: no, la demo scema \/ right keys at the right time