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

["Till Varoquaux" <till.varoquaux@gmail.com>]

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 <mwh@cs.umd.edu> 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 <garrigue@math.nagoya-
> > u.ac.jp> wrote:
> >> From: Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>
> >>
> >>> 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/