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

[Michael Hicks <mwh@cs.umd.edu>]

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