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

["Christopher L Conway" <cconway@cs.nyu.edu>]

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
>
>