From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <darioteixeira@yahoo.com>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: **
X-Spam-Status: No, score=2.8 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE,
	DNS_FROM_RFC_POST,DNS_FROM_RFC_WHOIS,DNS_FROM_SECURITYSAGE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
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 1C246BB84
	for <caml-list@yquem.inria.fr>; Fri, 31 Oct 2008 15:05:55 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AjQBAEOtCknOvjGskWdsb2JhbACUDgEBAQEJCwoHEQOtQotABQIBg06DLQ
X-IronPort-AV: E=Sophos;i="4.33,522,1220220000"; 
   d="scan'208";a="19425481"
Received: from web54602.mail.re2.yahoo.com ([206.190.49.172])
  by mail1-smtp-roc.national.inria.fr with SMTP; 31 Oct 2008 15:05:54 +0100
Received: (qmail 7569 invoked by uid 60001); 31 Oct 2008 14:05:53 -0000
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws;
  s=s1024; d=yahoo.com;
  h=X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID;
  b=OhxFwUDRYW8Gl2jGOEFkah/TUWtgAWTwP3DMa3uGxN7rknla3kYBS78JA7qXI6nvBZbLM1gsN3AiM9QTARPzQwj899g8Rrcm9Y8NZ5VAbS4BvUgWh55GBTu9kWHzQAhmaT0hBrQU8Gzag7HfpcQTko8euavsN0RB9GtWyA6x470=;
X-YMail-OSG: lyycQLQVM1nQWd60bf_vYwLD0LiRWpQ2VjtW_xhc3aRjaEIKMDVWR835kGpZhWCTaEJBheWI.bvCA8tHM7w61dZBLWIJdkcDr_JBRFmCzHwCxhibqqrxHN_bqyT2iPY_VBoXYugj_9.5k_ljLhNOPlF6HLa6.aBgIUnTNmqY
Received: from [213.205.71.59] by web54602.mail.re2.yahoo.com via HTTP; Fri, 31 Oct 2008 07:05:53 PDT
X-Mailer: YahooMailWebService/0.7.247.3
Date: Fri, 31 Oct 2008 07:05:53 -0700 (PDT)
From: Dario Teixeira <darioteixeira@yahoo.com>
Subject: Re: [Caml-list] Private types
To: dra-news@metastack.com,
	Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Cc: caml-list@yquem.inria.fr
In-Reply-To: <20081031.090842.254669920.garrigue@math.nagoya-u.ac.jp>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Message-ID: <761104.6489.qm@web54602.mail.re2.yahoo.com>
X-Spam: no; 0.00; subtyping:01 unification:01 subtyping:01 coerced:01 unification:01 foobar:01 foobar:01 sig:01 foo:01 foo:01 val:01 val:01 bool:01 bool:01 struct:01 

Hi,

> Your intuition is correct that it would theoretically be possible to
> try subtyping in place of unification in some cases. The trouble is
> that thoses cases are not easy to specify (so that it would be hard
> for the programmer to known when he can remove a coercion), and that
> subtyping is potentially very costly (structural subtyping is much
> harder to check than the nominal subtyping you have in Java.)


Thanks for the explanation, Jacques.  If I understand correctly, by requiri=
ng
subtyping relations to be explicitly coerced, the "giant system of equation=
s"
behind unification can be simplified because it doesn't need to worry about
all possible subtyping relations.  So in a sense this is also a matter of
computational tractability, right?

I have also been playing with 3.11's private types, and I would like to
share a problem I've come across.  Suppose I have a Foobar module defined
as follows (note the use of a type constraint):


module Foobar:
sig
=09type foo_t =3D [ `A ]
=09type bar_t =3D [ `B ]
=09type foobar_t =3D [ foo_t | bar_t ]
=09type 'a t =3D 'a constraint 'a =3D [< foobar_t ]

=09val make_a: unit -> foo_t t
=09val make_b: unit -> bar_t t
=09val is_foo: [< foobar_t] t -> bool
=09val is_bar: [< foobar_t] t -> bool
end =3D
struct
=09type foo_t =3D [ `A ]
=09type bar_t =3D [ `B ]
=09type foobar_t =3D [ foo_t | bar_t ]
=09type 'a t =3D 'a constraint 'a =3D [< foobar_t ]

=09let make_a () =3D `A
=09let make_b () =3D `B
=09let is_foo =3D function `A -> true | `B -> false
=09let is_bar =3D function `B -> true | `A -> false
end


Suppose also that I want to define a "is_foo" function in an external modul=
e.
This function only needs to pattern-match on Foobar.t values.  The followin=
g
code will work:

module Mymod:
sig
=09open Foobar

=09val is_foo2: [< foobar_t] t -> bool
end =3D
struct
=09let is_foo2 =3D function `A -> true | `B -> false
end


But now consider that I want to enforce the creation of Foobar.t values onl=
y
via Foobar's constructor functions, but I would like to keep the possibilit=
y of
external modules to pattern-match on Foobar.t values.  In other words, chan=
ge
Foobar but don't break Mymod.  The immediate (na=EFve) solution is to make
use of private types, thus changing the signature of Foobar to the followin=
g:


module Foobar:
sig
=09type foo_t =3D [ `A ]
=09type bar_t =3D [ `B ]
=09type foobar_t =3D [ foo_t | bar_t ]
=09type 'a t =3D private 'a constraint 'a =3D [< foobar_t ]

=09val make_a: unit -> foo_t t
=09val make_b: unit -> bar_t t
=09val is_foo: [< foobar_t] t -> bool
=09val is_bar: [< foobar_t] t -> bool
end =3D (...)


But this will break Mymod.  The compile will complain with the following er=
ror:

      Values do not match:
         val is_foo2 : [< `A | `B ] -> bool
       is not included in
         val is_foo2 : [< Foobar.foobar_t ] Foobar.t -> bool

Any ideas on how can I get around this problem?

Thanks!
Cheers,
Dario Teixeira
=0A=0A=0A