type unsoundness with constraints and polymorphic variants

type unsoundness with constraints and polymorphic variants

[Stephen Weeks]

We've hit a type unsoundness in OCaml that can easily cause a segfault
at runtime.  It came up in some code that uses phantom types to
express whether or not a structure can be mutated and the identity
functions to convert from a read-write object to a read-only view.

Here is a distillation of the bug.  If you compile this, you get a
warning about line 11 being an unused case.  If you then run the
resulting executable, you get a segfault.

--------------------------------------------------------------------------------
type 'a t = 'a constraint 'a = [< `X | `Y of unit -> unit ]

module M : sig
  val f : 'a t -> [ `Y of unit -> unit ] t
end = struct
  let f x = x
end

let () =
  match M.f `X with
  | `X -> ()  (* line 11 *)
  | `Y f -> f ()

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

[Markus Mottl]

On Feb 11, 2008 3:03 PM, Stephen Weeks <sweeks@janestcapital.com> wrote:
> Here is a distillation of the bug.  If you compile this, you get a
> warning about line 11 being an unused case.  If you then run the
> resulting executable, you get a segfault.

Line 11 can obviously be deleted, the segfault still persists.  The
unsoundness seems to appear when the signature constraint is applied
to the module.  It should fail, because the identity function is
clearly not a valid instance of this type, since `X can be passed to
it and it would just be returned, thus violating the return type.

It seems that constraints on polymorphic variables are not handled
correctly during the unification of the contents of the module with
its signature.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

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

[Jacques Garrigue]

From: "Stephen Weeks" <sweeks@janestcapital.com>
> We've hit a type unsoundness in OCaml that can easily cause a segfault
> at runtime.  It came up in some code that uses phantom types to
> express whether or not a structure can be mutated and the identity
> functions to convert from a read-write object to a read-only view.
> 
> Here is a distillation of the bug.  If you compile this, you get a
> warning about line 11 being an unused case.  If you then run the
> resulting executable, you get a segfault.
> 
> -----------------------------------------------------------------------------
> type 'a t = 'a constraint 'a = [< `X | `Y of unit -> unit ]
> 
> module M : sig
>   val f : 'a t -> [ `Y of unit -> unit ] t
> end = struct
>   let f x = x
> end
> 
> let () =
>   match M.f `X with
>   | `X -> ()  (* line 11 *)
>   | `Y f -> f ()

Thanks for the report. It's so clearly a bug that it's strange it was
not found earlier :-(
A shorter version (without constraints) is:

  module M : sig val f : [< `A | `B] -> [`A] end = struct let f x = x end

This is now fixed in CVS, and should go in 3.10.2.

Cheers,

Jacques Garrigue

BTW, there is a bug tracking system...

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

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

Andrej

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

[Luc Maranget]

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

As far as I can remember,

First, Xavier made the type system, but we ignore where was God at the time.

We can perhaps assume that God let man invent any type system, provided
it is sound and admit principal types.

Then Xavier founded a church...

-- 
Luc

PS> you can have a look at Xavier's thesis, but you'll find nothing
     on polymorphic variants there.

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

[Jacques Garrigue]

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

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

[Christopher L Conway]

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

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

[Michael Hicks]

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

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

[David Teller]

Looks waaay to expert for a Summer of Code.

Cheers,
 David

On Wed, 2008-02-13 at 09:18 -0500, Michael Hicks 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

-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act
brings liquidations. 

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

[Till Varoquaux]

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/

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

[Michael Hicks]

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

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

[Mattias Engdegård]

>I would be very impressed if a student managed to write a full formal
>semantic in a summer.

So would most people, but we may be missing the goal. A solid
understanding of the language for serious programming or even
independent reimplementation does not necessarily require formal
semantics. A careful prose description would probably do.

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

[Christopher L Conway]

On Feb 13, 2008 9:53 AM, Mattias Engdegård <mattias@virtutech.se> wrote:
> >I would be very impressed if a student managed to write a full formal
> >semantic in a summer.
>
> So would most people, but we may be missing the goal. A solid
> understanding of the language for serious programming or even
> independent reimplementation does not necessarily require formal
> semantics. A careful prose description would probably do.

A careful prose description is what I intended to propose. A true
formal semantics is neither necessary nor sufficient.

Chris

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

[Stefano Zacchiroli]

On Wed, Feb 13, 2008 at 02:35:50PM +0000, Till Varoquaux wrote:
> AFAIK SML is the only language that has a formal semantic. ECMA script
> might get one soon (a reference SML interpreter).

I don't think anybody asked for a formal semantics. Of course it might
be something *really* useful, but for the purpose of a user manual
(where with "user" I mean Random J OCaml developer) a rigorous prose
would be enough. It is still something we are missing for OCaml.

Just because you mentioned examples, another example is Python. It has
no formal semantics AFAIK, but still the reference manual describes the
data model of values the programmer can depict in her mind to understand
the current interpreter status. Then, each language feature is described
by giving its grammar entry in the global language grammar, and its
semantics is described---with prose---in terms of modifications of such
a status.  (And of course we don't like such a description since we are
functional programmers, but that's another issue.)

I'm not that inside the Haskell world, but the Haskell report seems to
be something really similar.

Why should we be lacking behind such reference manuals, especially
considering that the roots of our language reside in formal papers
already published somewhere, is something which keeps astonishing me.

Cheers.

-- 
Stefano Zacchiroli -*- PhD in Computer Science ............... now what?
zack@{upsilon.cc,cs.unibo.it,debian.org}  -<%>-  http://upsilon.cc/zack/
(15:56:48)  Zack: e la demo dema ?    /\    All one has to do is hit the
(15:57:15)  Bac: no, la demo scema    \/    right keys at the right time