From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id E5A8EBC6B for ; Tue, 12 Feb 2008 15:43:59 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAEM/sUfAXQInh2dsb2JhbACQOwEBAQgKKZtS X-IronPort-AV: E=Sophos;i="4.25,341,1199660400"; d="scan'208";a="22540204" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 12 Feb 2008 15:44:05 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1CEhtP2029875 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 12 Feb 2008 15:43:59 +0100 From: luc.maranget@inria.fr (Luc Maranget) X-IronPort-AV: E=Sophos;i="4.25,341,1199660400"; d="scan'208";a="9100841" Received: from yquem.inria.fr ([128.93.8.37]) by mail3-relais-sop.national.inria.fr with ESMTP; 12 Feb 2008 15:43:58 +0100 Received: by yquem.inria.fr (Postfix, from userid 18041) id D808DBC6B; Tue, 12 Feb 2008 15:43:58 +0100 (CET) Date: Tue, 12 Feb 2008 15:43:58 +0100 To: Andrej.Bauer@andrej.com Cc: Caml Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants Message-ID: <20080212144358.GB9807@yquem.inria.fr> References: <18352.43565.401296.820373@nyc-qws-r03.delacy.com> <20080212.132225.27792058.garrigue@math.nagoya-u.ac.jp> <47B17667.2090907@fmf.uni-lj.si> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <47B17667.2090907@fmf.uni-lj.si> User-Agent: Mutt/1.5.9i X-Miltered: at concorde with ID 47B1B0AB.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; maranget:01 maranget:01 variants:01 ocaml:01 compiler:01 ocaml:01 formalized:01 compiler:01 andrej:01 xavier's:01 variants:01 polymorphic:01 polymorphic:01 typing:01 luc:01 > 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.