Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: 2008-02-13 (14:18)
From: Michael Hicks <mwh@c...>
Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants
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 ...


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 < 
>> wrote:
>> From: Andrej Bauer <>
>>> 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:
>> Archives:
>> Beginner's list:
>> Bug reports:
> _______________________________________________
> Caml-list mailing list. Subscription management:
> Archives:
> Beginner's list:
> Bug reports: