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-12 (14:44)
From: luc.maranget@i...
Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants
> 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...


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