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 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr 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 DD247BBC1 for ; Mon, 18 Feb 2008 17:44:45 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJ5EuUeCcYARl2dsb2JhbACMO4QcAQEBAQEGBAYJCBibAQ X-IronPort-AV: E=Sophos;i="4.25,372,1199660400"; d="scan'208";a="7433527" Received: from coriana6.cis.mcmaster.ca ([130.113.128.17]) by mail2-smtp-roc.national.inria.fr with ESMTP; 18 Feb 2008 17:44:45 +0100 Received: from Gorash7.UTS.McMaster.CA (Gorash7.UTS.mcmaster.ca [130.113.196.61]) by coriana6.cis.mcmaster.ca (8.13.7/8.13.7) with ESMTP id m1IGi9qP022165; Mon, 18 Feb 2008 11:44:26 -0500 (EST) Received: from cgpsrv2.cis.mcmaster.ca (univmail.CIS.McMaster.CA [130.113.64.46]) by Gorash7.UTS.McMaster.CA (8.13.7/8.13.7) with ESMTP id m1IGi0jD023735; Mon, 18 Feb 2008 11:44:01 -0500 Received: from [99.235.248.61] (account carette@univmail.cis.mcmaster.ca HELO [192.168.1.101]) by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro SMTP 4.3.12) with ESMTPSA id 201672680; Mon, 18 Feb 2008 11:44:01 -0500 Message-ID: <47B9B5D9.5010303@mcmaster.ca> Date: Mon, 18 Feb 2008 11:44:09 -0500 From: Jacques Carette Organization: McMaster University User-Agent: Thunderbird 2.0.0.9 (Windows/20071031) MIME-Version: 1.0 To: Jacques Garrigue Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Formal specifications of programming languages References: <47B348F6.6010607@fmf.uni-lj.si> <47B40514.3070906@inria.fr> <4a051d930802150630l20f46d17g153842c2cd70b1c2@mail.gmail.com> <20080218.190529.45878855.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20080218.190529.45878855.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-PMX-Version-Mac: 5.4.1.325704, Antispam-Engine: 2.6.0.325393, Antispam-Data: 2008.2.18.83227 X-PerlMx-Spam: Gauge=IIIIIII, Probability=7%, Report='__CT 0, __CTE 0, __CT_TEXT_PLAIN 0, __HAS_MSGID 0, __MIME_TEXT_ONLY 0, __MIME_VERSION 0, __SANE_MSGID 0, __USER_AGENT 0, __pbl.spamhaus.org_TIMEOUT ' X-Spam: no; 0.00; functors:01 wrote:01 abstract:01 abstract:01 encode:01 caml-list:01 modules:02 mcmaster:02 garrigue:03 seems:03 module:03 module:03 jacques:03 jacques:03 languages:03 Jacques Garrigue wrote: > (Actually, abstract types in modules can also be seen as existentials, > but I don't think this is what you are talking about.) > This is a subtle issue that I have yet to understand 'completely'. Can you expand on this "can also be seen as existentials" please? To me, there seems to be a difference between these, but I have never been able to quite put my finger on it. It may be because they are not really different, ie both can encode the other. This is not just an idle question. In two separate papers (with co-authors), abstract types in module types (and Functors) are used as what I think of as "constrained existentials", to good effect. But maybe I really ought to think of those as "for all types that can be used as implementations of this signature" rather than "some _specific_ type that satisfies this signature". I say 'specific' because while users of the module cannot see the implementation, inside the implementation, the actual representation is rather crucial. Jacques Carette