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=none autolearn=disabled version=3.1.3 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 61E05BC69 for ; Fri, 16 Nov 2007 10:12:55 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHPtPEfAXQInh2dsb2JhbACPCgEBAQgKKQ X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="4560078" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 16 Nov 2007 10:12:55 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id lAG9CsQt023360 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 16 Nov 2007 10:12:55 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAHPtPEfBAkMt/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="19373721" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail4-smtp-sop.national.inria.fr with ESMTP; 16 Nov 2007 10:12:54 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 8F6481DDB5A; Fri, 16 Nov 2007 10:12:53 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id EwccJAzs0rqc; Fri, 16 Nov 2007 10:12:50 +0100 (CET) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id C4D481E53E0; Fri, 16 Nov 2007 10:12:48 +0100 (CET) Message-ID: <473D5F33.1000904@fmf.uni-lj.si> Date: Fri, 16 Nov 2007 10:13:23 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 2.0.0.6 (X11/20071022) MIME-Version: 1.0 To: =?ISO-8859-2?Q?Jean-Christophe_Filli=E2tre?= , Caml Subject: Re: [Caml-list] Compiler feature - useful or not? References: <20071114184352.GB28796@yquem.inria.fr> <473BE750.9060301@frisch.fr> <20071115132649.GB15754@yquem.inria.fr> <20071116.014620.919650100.Christophe.Troestler+ocaml@umh.ac.be> <473D5380.2010508@fmf.uni-lj.si> <473D5BAD.10409@lri.fr> In-Reply-To: <473D5BAD.10409@lri.fr> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 473D5F16.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 compiler:01 filliatre:01 functor:01 sig:01 val:01 ocaml:01 coq:01 rig:98 wrote:01 caml-list:01 pair:01 module:03 embedding:03 Jean-Christophe Filliātre wrote: > Despite the embedding you're mentioning, which could be added as follows > > module type ConstructRing = > functor (M : RIG) -> sig include RING val embed : M.t -> t end > > I don't see what else you could add to the signature (unless you want to > expose that the type t of the RING is a pair of type M.t * M.t; and even > with that you couldn't expose the definitions of the operations in the > signature). > > All the properties you're expecting for the resulting ring are part of > (logical) specifications, which cannot be expressed via ocaml types. > You could do that in a richer type system (e.g. Coq). Not quite. The universal property of the resulting ring R is this: for any ring T, if f : M -> T is a function preserving 0, + and * then there is a unique function g : R -> T preserving 0, +, * and - such that g (include x) = f x, where include is as above. This needs to be accounted for, and it's not just a logical specification. Andrej