From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 53283BC57 for ; Thu, 16 Dec 2010 17:03:43 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ak8BAAPHCU2LEwExe2dsb2JhbACkOBUBARYiBR+zLgGOOgWFSosB X-IronPort-AV: E=Sophos;i="4.59,355,1288566000"; d="scan'208";a="82916033" Received: from hera.mpi-sb.mpg.de ([139.19.1.49]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 16 Dec 2010 17:03:43 +0100 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=Message-ID:In-Reply-To: References:Date:Subject:From:To:Cc:MIME-Version:Content-Type: Content-Transfer-Encoding; bh=rvqxLx2Z9R6Ze7q7G80cDq80wUmtq5pRyF 8fzL/1rtM=; b=t2aKs1zpSvvDyHyJDgC9JNo8DcR2fB2DwriO/Qtm6q+12cBQXT 3RHwzxmDYxJPZURE3m9Vn+RiOWX8vbAV7mcr1QTWYko5WOc/dHFiA3ZQLidU5XNF g4lMd43kXbnm9HXnLAMBgpMDimujN15SDpaJwqGyJEGJmR1Bv0YlPCj0Q= Received: from infao0525.mpi-klsb.mpg.de ([139.19.1.26]:52024 helo=maniac.mpi-klsb.mpg.de) by hera.mpi-sb.mpg.de (envelope-from ) with esmtp (Exim 4.69) id 1PTGIr-00019c-CL; Thu, 16 Dec 2010 17:03:39 +0100 Received: from local by maniac.mpi-klsb.mpg.de (envelope-from ) with local (Exim 4.69) id 1PTGIq-0001TA-SK; Thu, 16 Dec 2010 17:03:37 +0100 Received: from 74.125.57.233 (SquirrelMail authenticated user rossberg) by mail.mpi-sws.org with HTTP; Thu, 16 Dec 2010 17:03:37 +0100 (CET) Message-ID: In-Reply-To: <4D0A2D24.8090401@frisch.fr> References: <4D0A14BE.9080305@mlstate.com> <4D0A2D24.8090401@frisch.fr> Date: Thu, 16 Dec 2010 17:03:37 +0100 (CET) Subject: Re: [Caml-list] Implicitely abstracted type From: rossberg@mpi-sws.org To: "Alain Frisch" Cc: "Louis Gesbert" , caml-list@inria.fr User-Agent: SquirrelMail/1.4.15 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-15 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal X-Spam: no; 0.00; abstracted:01 rossberg:01 frisch:01 functor:01 functor:01 supertype:01 supertype:01 wrote:01 andreas:01 caml-list:01 alain:01 module:03 module:03 computing:05 computing:05 Alain Frisch wrote: > > When applying a functor of type > functor(X:S1) -> S2 to a module of type T, the module type for the > result can be obtained in two different ways: > > (1) T is a path: the module type is obtained by substituting X with T in S2. > > (2) T is not a path: the module type is obtained by computing the > smallest supertype of S2 that doesn't contain X anymore (under the extra > assumption that X has type T). I believe this doesn't type-check. :) You probably meant to say: "When applying a functor of type functor(X:S1) -> S2 to a module M of type T, the module type for the result can be obtained in two different ways: (1) M is a path: the module type is obtained by substituting X with M in S2. (2) M is not a path: the module type is obtained by computing the smallest supertype of S2 that doesn't contain X anymore (under the extra assumption that X has type T)." /Andreas