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=1.6 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL autolearn=disabled version=3.1.3 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 5B80ABBC1 for ; Tue, 19 Feb 2008 09:57:15 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAIQoukfAXQImh2dsb2JhbACPV3YBAQEICimccw X-IronPort-AV: E=Sophos;i="4.25,375,1199660400"; d="scan'208";a="9335324" Received: from discorde.inria.fr ([192.93.2.38]) by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Feb 2008 09:57:15 +0100 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1J8vEjq004831 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 19 Feb 2008 09:57:14 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAOYoukfAEKcgh2dsb2JhbACPV3YBAQEICimcbA X-IronPort-AV: E=Sophos;i="4.25,375,1199660400"; d="scan'208";a="8256193" Received: from selenite.metnet.navy.mil ([192.16.167.32]) by mail1-smtp-roc.national.inria.fr with ESMTP; 19 Feb 2008 09:57:13 +0100 Received: (qmail 3857 invoked by uid 107); 19 Feb 2008 08:57:11 -0000 Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.152) by selenite.metnet.navy.mil with SMTP; 19 Feb 2008 08:57:11 -0000 Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id B7350A99B; Tue, 19 Feb 2008 00:54:23 -0800 (PST) From: oleg@okmij.org To: caml-list@inria.fr Subject: Re: existentials [was: Formal specifications of programming languages] Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org Message-Id: <20080219085423.B7350A99B@Adric.metnet.fnmoc.navy.mil> Date: Tue, 19 Feb 2008 00:54:23 -0800 (PST) X-Miltered: at discorde with ID 47BA99EA.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 ocaml:01 existential:01 integers:01 coercions:01 ocaml:01 existential:01 'self:01 'self:01 val:01 val:01 iter:01 printf:01 printf:01 aab:98 Jacques Garrigue wrote: > There are no existentials in ocaml, only first-class universal types > (in polymorphic methods and polymorphic record fields.) Surely object types are existentials with respect to the types of their fields?! Wasn't it the very motivation of objects -- encapsulation -- to abstract over the types of the fields and so prevent the outsiders from finding out not only the values of the fields but also their types. Outsiders should only use the methods of the object and should know nothing about object's fields, if any. As the illustration, here is the standard counter example, defining one existential type and two its values. The values use two different representations of the internal state of the counter: a pair of integers and a float. This state is not observable: and so we can place the two counter objects in the same list without any need for coercions. OCaml knows that the state is not observable and so the two objects have the same type, difference in the type of their state notwithstanding. One must say that exactly the same example has been implemented without any existentials whatsoever: Eliminating existentials, finally Caml-list, Nov 14, 2007 http://caml.inria.fr/pub/ml-archives/caml-list/2007/11/dcd3aab066b5f28852db8ccaf35d35d7.en.html which poses the question if existentials are really needed. On with the example: the declaration of the existential type class type counter = object ('self) method observe : int method step : unit -> 'self end;; Here are two different counters, with two different representations of the internal state (a pair of int, or a float). let counter1 = object val seed = 0 val upper = 5 method observe = seed method step () = let new_seed = if seed >= upper then 0 else succ seed in {< seed = new_seed >} end;; (* use FP seed *) let counter2 = object val seed = 0.0 method observe = int_of_float (10.0 *. seed) method step () = {< seed = cos seed >} end;; We can place them into a list let lst = [counter1; counter2];; and iterate over: let advance_all = List.map (fun c -> c#step ());; let show_all = List.iter (fun c -> Printf.printf "%d\n" c#observe);; let test = let () = show_all lst in let () = show_all (advance_all (advance_all lst)) in ();; result: 0 0 2 5 val test : unit = ()