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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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