Re: [Caml-list] type unsoundness with constraints and polymorphic variants

[Stefano Zacchiroli <zack@upsilon.cc>]

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