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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 96A11BC69 for ; Fri, 16 Nov 2007 09:58:26 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAKLqPEfAXQImh2dsb2JhbACPCgEBAQgKKQ X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="4318189" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 16 Nov 2007 09:58:26 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id lAG8wPNN028343 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 16 Nov 2007 09:58:26 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAO7pPEeBrw8E/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="19372952" Received: from ext.lri.fr ([129.175.15.4]) by mail4-smtp-sop.national.inria.fr with ESMTP; 16 Nov 2007 09:58:25 +0100 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id 9810BA4692; Fri, 16 Nov 2007 09:58:25 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id NoIlwtRqiA3r; Fri, 16 Nov 2007 09:58:25 +0100 (CET) Received: from [192.168.0.10] (mry91-1-82-229-156-20.fbx.proxad.net [82.229.156.20]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id 48DA9A463B; Fri, 16 Nov 2007 09:58:25 +0100 (CET) Message-ID: <473D5BAD.10409@lri.fr> Date: Fri, 16 Nov 2007 09:58:21 +0100 From: =?ISO-8859-2?Q?Jean-Christophe_Filli=E2tre?= User-Agent: Thunderbird 1.5.0.14pre (X11/20071022) MIME-Version: 1.0 To: Andrej.Bauer@andrej.com Cc: Christophe TROESTLER , 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> In-Reply-To: <473D5380.2010508@fmf.uni-lj.si> X-Enigmail-Version: 0.94.2.0 OpenPGP: url=http://www.lri.fr/~filliatr/mykey.asc Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 8bit X-Miltered: at discorde with ID 473D5BB1.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatre:01 lri:01 compiler:01 andrej:01 functor:01 functor:01 sig:01 val:01 ocaml:01 coq:01 rig:98 rig:98 caml-list:01 pair:01 Andrej Bauer a écrit : > The puzzle is this: write down the module type for the construction > taking a rig and returning the free ring over it. It is _not_ just > > module type ConstructRing = functor (M : RIG) -> RING > > because that would allow _any_ ring whatsoever as the result. It has to > be the ring that comes from M via above construction, so there has to be > extra stuff, such as an embedding of M into the resulting R. But what else? 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). But may be I misunderstood your question... -- Jean-Christophe