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

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

I didn't mean to suggest that the entire language be formalized in a  
summer!  I was implying that PL theory people (many of whose graduate  
students use OCaml) might have some reason to get involved with the  
project Chris proposed, and the Jane Street funding might be a  
vehicle for that via their students.  There are a lot of smart  
graduate students that monitor this list (I have a few!).

-Mike

On Feb 13, 2008, at 9:35 AM, Till Varoquaux wrote:

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