Version française
Home     About     Download     Resources     Contact us    
Browse thread
type unsoundness with constraints and polymorphic variants
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Till Varoquaux <till.varoquaux@g...>
Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants
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/