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
Formal specifications of programming languages
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2008-02-18 (10:05)
From: Jacques Garrigue <garrigue@m...>
Subject: Re: [Caml-list] Formal specifications of programming languages
From: "Christopher L Conway" <>

> Do any of these papers address existentials?

There are no existentials in ocaml, only first-class universal types
(in polymorphic methods and polymorphic record fields.)
Universal types can be used to encode existentials through the usual
dual encoding.
The theory behind polymorpic methods is described in my paper with
Didier Remy, in the Objects section. Polymorphic fields in records are
simpler, and they were already formalized in earlier papers by Didier

(Actually, abstract types in modules can also be seen as existentials,
but I don't think this is what you are talking about.)

Jacques Garrigue