From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id D5A64BBAF for ; Thu, 12 Aug 2010 02:21:45 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArsBAMPbYkzRVdY0kGdsb2JhbACgMQgVAQEBAQkJDAcRAx+iFYkQghGGGi6IVAEBAwWFNQSJUA X-IronPort-AV: E=Sophos;i="4.55,355,1278280800"; d="scan'208";a="65297506" Received: from mail-bw0-f52.google.com ([209.85.214.52]) by mail1-smtp-roc.national.inria.fr with ESMTP; 12 Aug 2010 02:21:44 +0200 Received: by bwz17 with SMTP id 17so585034bwz.39 for ; Wed, 11 Aug 2010 17:21:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:in-reply-to :references:date:message-id:subject:from:to:cc:content-type; bh=HSC2ggGX7Fq4/90PF0J2JBnm5UioUk62vuTT8GuB4tA=; b=JZsnfLlhtpQANfEdtuRb8Q1XuKnnh25bLNVzr+XQvTHMWOgNUHn4Yn7wB3mP4332An rT0H0MtxEA9Z3wfAqm0HOskqachE69lWWxGBskemubvESfA6bvDBQOJzuSUZeBEOTSzI RWewoSFEftZM8MFnaItpcCUgLPnDuk7WrGfIM= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=M73z59K0kul/4uMftf03FbR6/jrL3RCM93DCL8R1Vq8MQt1PhTMuXLKWxr6bJyvJKq VXZWdXTybvwiu4plU+VJFb+z4t6lEwa3U1n622zBpWjKF5azXBvIJaAsgUeIcdWicr31 BmeYDbuRe3cr3ysWOrWXy2M7+xFKEAbB15JII= MIME-Version: 1.0 Received: by 10.204.22.74 with SMTP id m10mr72775bkb.63.1281572503991; Wed, 11 Aug 2010 17:21:43 -0700 (PDT) Received: by 10.204.54.68 with HTTP; Wed, 11 Aug 2010 17:21:43 -0700 (PDT) In-Reply-To: <03fb01cb3955$76093770$621ba650$@com> References: <877hk1m1df.fsf@mid.deneb.enyo.de> <87bp9dkkca.fsf@mid.deneb.enyo.de> <4c5f194e.8644d80a.7fef.69e6@mx.google.com> <03fb01cb3955$76093770$621ba650$@com> Date: Wed, 11 Aug 2010 20:21:43 -0400 Message-ID: Subject: Re: [Caml-list] interest in a much simpler, but modern, Caml? From: Jeremy Bem To: Jon Harrop Cc: bluestorm , caml-list List , Florian Weimer Content-Type: multipart/alternative; boundary=000325555ec6dac3c5048d9559c9 X-Spam: no; 0.00; ocaml's:01 runtime:01 abstraction:01 ocamllex:01 pervasives:01 syntax:01 ocaml:01 overloading:01 minimalist:01 higher-order:01 pervasives:01 foo:01 foo:01 runtime:01 lacks:01 --000325555ec6dac3c5048d9559c9 Content-Type: text/plain; charset=ISO-8859-1 On Wed, Aug 11, 2010 at 9:02 AM, Jon Harrop < jonathandeanharrop@googlemail.com> wrote: > > What happens when you do: > > if Int.(x = 42 || x = 45) then ... else ... > > Presumably it either barfs on the assumption that "||" refers to bitwise-or > between ints, or we're back to inventing progressively more absurd operator > names for each individual combination of types over which they might work. > How so? I think this is a borderline case (even in C++, "||" does not refer to bitwise-or). But even if Int.(||) *were* defined as some sort of integer operation, one could simply write: if Int.(x = 42) || Int.(x = 45) Also, I think the discussion has shifted. For me, the local open is a reasonably appealing way to stop using OCaml's exotic polymorphic operators whose behavior depends on the runtime representation and which don't respect type abstraction. (For example, ocamllex uses Pervasives.(=) to test whether Map's are empty, but this breaks if the Map representation changes.) Moreover the syntax even maintains OCaml compatibility thanks to the recent update. But now we seem to be talking about operator overloading, and I'm just not convinced it's necessary at all in a system with a minimalist aesthetic. Back to the local opens, I find that I'm hesitant to add so many of them, especially for equality. Polymorphic equality is hardly unnatural, after all (cf. higher-order logic). I wonder, do any practical languages use quotient types to implement custom equality predicates? In principle, Pervasives.(=) ought to be the "finest" reasonable equivalence relation on a type, which could then be coarsened: type foo = Foo of int | Goo of string let _ = assert (Foo 3 <> Goo "3") (* duh *) let foo_equiv x y = match x, y with Foo a, Foo b -> a=b | Goo a, Goo b -> a=b | Foo a, Goo b | Goo b, Foo a -> string_of_int a = b type goo = foo / foo_equiv (* automatically creates goo_of_foo *) let _ = assert (goo_of_foo (Foo 3) = goo_of_foo (Goo "3")) This would require runtime support. I envision that every "goo" is a block whose tag is "Quotient_tag" and which stores a "foo_equiv" closure in its first Obj field. As it happens, this approach would dovetail with my plans for an integrated proof assistant. Of course it lacks the "conservatism" I've been promoting :) -Jeremy --000325555ec6dac3c5048d9559c9 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable On Wed, Aug 11, 2010 at 9:02 AM, Jon Harrop <jonathandeanharrop@googlemail= .com> wrote:

What happens when you do:

=A0if Int.(x =3D 42 || x =3D 45) then ... else ...

Presumably it either barfs on the assumption that "||" refers to = bitwise-or
between ints, or we're back to inventing progressively more absurd oper= ator
names for each individual combination of types over which they might work.<= br>

How so? =A0I think this is a borderline= case (even in C++, "||" does not refer to bitwise-or). =A0But ev= en if Int.(||) *were* defined as some sort of integer operation, one could = simply write:
=A0=A0if Int.(x =3D 42) || Int.(x =3D 45)

Also, I think the discussion has shifted. =A0For me, the local open is a= reasonably appealing way to stop using OCaml's exotic polymorphic oper= ators whose behavior depends on the runtime representation and which don= 9;t respect type abstraction. =A0(For example, ocamllex uses Pervasives.(= =3D) to test whether Map's are empty, but this breaks if the Map repres= entation changes.) =A0Moreover the syntax even maintains OCaml compatibilit= y thanks to the recent update. =A0But now we seem to be talking about opera= tor overloading, and I'm just not convinced it's necessary at all i= n a system with a minimalist aesthetic.

Back to the local opens, I find that I'm hesitant t= o add so many of them, especially for equality. =A0Polymorphic equality is = hardly unnatural, after all (cf. higher-order logic). =A0I wonder, do any p= ractical languages use quotient types to implement custom equality predicat= es? =A0In principle, Pervasives.(=3D) ought to be the "finest" re= asonable equivalence relation on a type, which could then be coarsened:

type foo =3D Foo of int | Goo of string
let foo_equiv x y =3D
=A0=A0match x, y with
=A0=A0 =A0Foo a, Foo b -> a=3Db
=A0=A0| Goo a, Goo b -> a=3Db
=A0=A0| Foo a, Goo b=
= =A0=A0| Goo b, Foo a ->=A0string_of_int a =3D b
type go= o =3D foo / foo_equiv (* automatically creates goo_of_foo *)
let _ =3D assert (goo_of_foo (Foo 3) =3D goo_of_foo (Goo "3"= ))

This would require runtime support. =A0I= envision that every "goo" is a block whose tag is "Quotient= _tag" and which stores a "foo_equiv" closure in its first Ob= j field.

As it happens, this approach would dovetail with my pla= ns for an integrated proof assistant. =A0Of course it lacks the "conse= rvatism" I've been promoting :)

-Jeremy

--000325555ec6dac3c5048d9559c9--