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.6 required=5.0 tests=NO_REAL_NAME autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 9BA8BBB83 for ; Sun, 17 Sep 2006 07:08:35 +0200 (CEST) Received: from triton.rz.uni-saarland.de (triton.rz.uni-saarland.de [134.96.7.25]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k8H58ZP3018298 for ; Sun, 17 Sep 2006 07:08:35 +0200 Received: from uni-sb.de (uni-sb.de [134.96.7.230]) by triton.rz.uni-saarland.de (8.12.11.20060614/8.12.10) with ESMTP id k8H58Ppa21118375 for ; Sun, 17 Sep 2006 07:08:25 +0200 (CEST) Received: from mail.cs.uni-sb.de (mail.cs.uni-sb.de [134.96.254.200]) by uni-sb.de (8.13.8/2006081400) with ESMTP id k8H58PeQ009647 for ; Sun, 17 Sep 2006 07:08:25 +0200 (CEST) Received: from mail.ps.uni-sb.de (james.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.13.8/2006081400) with ESMTP id k8H58LFJ001504 for ; Sun, 17 Sep 2006 07:08:25 +0200 (CEST) Received: from localhost ([127.0.0.1] helo=www.ps.uni-sb.de ident=www-data) by mail.ps.uni-sb.de with esmtp (Exim 4.50) id 1GOotA-0002kt-LK for caml-list@inria.fr; Sun, 17 Sep 2006 07:08:21 +0200 Received: from 72.254.55.251 (SquirrelMail authenticated user rossberg) by www.ps.uni-sb.de with HTTP; Sun, 17 Sep 2006 07:08:20 +0200 (CEST) Message-ID: <1667.72.254.55.251.1158469700.squirrel@www.ps.uni-sb.de> In-Reply-To: References: <20060913091435.537F4AC04@Adric.metnet.fnmoc.navy.mil> Date: Sun, 17 Sep 2006 07:08:20 +0200 (CEST) From: rossberg@ps.uni-sb.de To: caml-list@inria.fr User-Agent: SquirrelMail/1.4.4 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal X-SA-Exim-Connect-IP: 127.0.0.1 X-SA-Exim-Mail-From: rossberg@ps.uni-sb.de Subject: Re: [Caml-list] Improper generic equality in Caml (Rossberg's SML vs Caml) X-SA-Exim-Version: 4.2 (built Thu, 03 Mar 2005 10:44:12 +0100) X-SA-Exim-Scanned: Yes (on mail.ps.uni-sb.de) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.5.1 (triton.rz.uni-saarland.de [134.96.7.25]); Sun, 17 Sep 2006 07:08:25 +0200 (CEST) X-AntiVirus: checked by AntiVir Milter (version: 1.1.3-1; AVE: 7.2.0.16; VDF: 6.36.0.29; host: AntiVir1) X-Miltered: at concorde with ID 450CD853.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; rossberg:01 improper:01 sml:01 rossberg:01 sml:01 ocaml:01 semantics:01 mutable:01 leibniz:01 ocaml's:01 pairs:01 ocaml's:01 implements:01 leibniz:01 ocaml:01 Diego Olivier Fernandez-Pons wrote: > > What does Andreas Rossberg in his SML vs. Caml page > > http://www.ps.uni-sb.de/~rossberg/SMLvsOcaml.html > > mean when he says that > > [Caml] Does not have a proper generic equality > on one hand (1, r) != (1, r), on the other (1, r) = (1, ref 1) To clarify: "proper" refers to "generic". The problem example is the one given on the left-hand side of the table. Let me elaborate. OCaml has two equalities: one fully structural, the other physical. Both work fine in special cases, but neither has the "right" semantics in the general case, where you deal with an arbitrary mixture of structural and mutable types. By "right" I mean equality in the standard Leibniz sense, where you can always replace equals with equals, without changing the outcome. Neither of OCaml's operators has this property. More conretely, given let r = ref 1 then the pairs (1, r) and (1, ref 1) are distinguishable by the effect of assignment. Still, OCaml's = considers them equal. On the other hand, it is not observable (by other means) whether the pair (1, r) is constructed once or twice, but == distinguishes these cases. Consequently, neither operator implements equality "correctly" on type (int * int ref), because either delivers a "wrong" result for one of these two examples. This problem can sometimes make translation from SML (which has Leibniz equality) to OCaml subtly difficult (that the inverse direction is potentially difficult is more obvious). Cheers, - Andreas