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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 2CF35BBC1 for ; Mon, 18 Feb 2008 22:48:10 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAHaLuUfUGypAi2dsb2JhbACBWYphhBwBAQEIAggJCAgJB5xk X-IronPort-AV: E=Sophos;i="4.25,373,1199660400"; d="scan'208";a="9324013" Received: from smtp7-g19.free.fr ([212.27.42.64]) by mail3-smtp-sop.national.inria.fr with ESMTP; 18 Feb 2008 22:48:10 +0100 Received: from smtp7-g19.free.fr (localhost [127.0.0.1]) by smtp7-g19.free.fr (Postfix) with ESMTP id 590ED322862; Mon, 18 Feb 2008 22:48:09 +0100 (CET) Received: from macbookpro.local (lns-bzn-48f-81-56-220-129.adsl.proxad.net [81.56.220.129]) by smtp7-g19.free.fr (Postfix) with ESMTP id AB2B9322859; Mon, 18 Feb 2008 22:48:08 +0100 (CET) Message-ID: <47B9FE15.4090900@univ-savoie.fr> Date: Mon, 18 Feb 2008 22:52:21 +0100 From: Christophe Raffalli User-Agent: Thunderbird 2.0.0.9 (Macintosh/20071031) MIME-Version: 1.0 To: Jacques Carette Cc: Jacques Garrigue , 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> <47B9B5D9.5010303@mcmaster.ca> In-Reply-To: <47B9B5D9.5010303@mcmaster.ca> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 functors:01 existential:01 existential:01 functor:01 beginner's:01 ocaml:01 bug:01 beginners:01 wrote:01 abstract:01 Jacques Carette a écrit : > 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. Abstract types are existential types with a projecton operator (like a choice operator) and they can have contraints. Unfortunatly, modules are not first class and you can not do a list of modules with the same signature but distinct implementation for their abstract types. This is the lack of first class modules that prevent to encode existential types using abstract types. The best to do is to use universal types in records with "the usual dual encoding" as said by J. Garrigues. Do not forget that an abstract type occurring in the signature of an argument to a functor is a universal type because it is "negated" ... > > Jacques Carette > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs