From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 440E5BC57 for ; Fri, 14 May 2010 23:33:41 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhwDAB9f7UtKfVM2emdsb2JhbACdfggVAQEUJAMfr2ABBY1oAQSFEI9A X-IronPort-AV: E=Sophos;i="4.53,233,1272837600"; d="scan'208";a="50640383" Received: from mail-gw0-f54.google.com ([74.125.83.54]) by mail3-smtp-sop.national.inria.fr with ESMTP; 14 May 2010 23:33:30 +0200 Received: by gwj16 with SMTP id 16so1646794gwj.27 for ; Fri, 14 May 2010 14:33:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=gamma; h=domainkey-signature:received:mime-version:received:in-reply-to :references:from:date:message-id:subject:to:cc:content-type; bh=m7lTGRuV9Ul1S2efFsDsV3lX9GJACaMWsBJN8CYldnc=; b=dgT03nfWWN/UB8joCOVFj958G++aTL+ILNvPrtxMFFuGgIDM3KJKxPSJGct0wYeNK3 NWBmnUw7VV0LC/MdLSJfVi6ZmxZq8Q25KQpsUnB1V7q3dHmOcdomtT3yf6KZN9F7/ZnG TQiRO5wp1CXaWdJfBsQXvUGYeGkqHvSFT0Dws= DomainKey-Signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=Uywjh/NiQoABNKA9rsQnhHlk4oYChm33v2N3HVGS3liJZ1YVnA/n75oYAAQ8I4nMQ6 yR/PNy6yCa5c0auwkLvCYpqKIrlH8DHIJcu721C+9ze579HoiQbB9IATTYxy0v/mBAT+ zezphizI1mmRtqil8DBAtI/u+TQqMPtaO4iyI= Received: by 10.101.132.12 with SMTP id j12mr1901505ann.130.1273872809100; Fri, 14 May 2010 14:33:29 -0700 (PDT) MIME-Version: 1.0 Received: by 10.100.109.11 with HTTP; Fri, 14 May 2010 14:33:09 -0700 (PDT) In-Reply-To: <20100515.004940.200940107.garrigue@math.nagoya-u.ac.jp> References: <20100515.004940.200940107.garrigue@math.nagoya-u.ac.jp> From: Philippe Veber Date: Fri, 14 May 2010 23:33:09 +0200 Message-ID: Subject: Re: [Caml-list] Closed variants, type constraints and module signature To: Jacques Garrigue Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=0016e68e91964686e2048694a0ab X-Spam: no; 0.00; variants:01 sig:01 val:01 sig:01 val:01 struct:01 mismatch:01 subtype:01 struct:01 mismatch:01 subtype:01 polymorphic:01 polymorphic:01 beginners:01 beginners:01 --0016e68e91964686e2048694a0ab Content-Type: text/plain; charset=ISO-8859-1 2010/5/14 Jacques Garrigue > From: Philippe Veber > > > I'd like to define a type with a variable that is constrained to accept > only > > polymorphic variant types included in a given set of tags. That is how I > > believed one should do : > > > > Objective Caml version 3.11.2 > > > > # type 'a t = 'a constraint 'a = [< `a | `b ];; > > type 'a t = 'a constraint 'a = [< `a | `b ] > > > > But I stumbled upon the following problem, when trying to use this > > definition > > > > > > # module type S = sig > > val v : 'a t > > end;; > > module type S = sig val v : [< `a | `b ] t end > > > > # module I : S = struct > > let v = `a > > end;; > > > > Error: Signature mismatch: > > Modules do not match: sig val v : [> `a ] end is not included in S > > Values do not match: > > val v : [> `a ] > > is not included in > > val v : [< `a | `b ] t > > > > Does anyone know why the definition of module I is rejected ? And if this > is > > the intended behavior, why does the following work ? > > > > # let v : 'a t = `a > > ;; > > val v : [< `a | `b > `a ] t = `a > > But it doesn't really work! > More precisely, the type [< `a | `b > `a ] t is an instance of 'a t, > not 'a t itself, an a module interface should give a type at most as > general as the implementation. > Right, I understand now there are two different mechanisms at hand here : in the module case, the type annotation for v is a specification, in the let binding case, it is a constraint. Seems like my question was better suited to beginners list ! Just to be sure : module I is rejected because v should have type 'a t for all 'a satisfying the constraint 'a = [< `a | `b ], that contain in particular [ `b ], which is incompatible with the type of v. Is that correct ? > > In your case, you should simply write > > type t = [`a | `b] > > since you don't know what v may be. > If i absolutely wanted to forbid other tags than `a and `b, while keeping the possibility to manage subtype hierarchies, maybe I could also change the code this way : type u = [`a | `b] type 'a t = 'a constraint 'a = [< u ] module type S = sig val v : u t val f : 'a t -> [`a] t end module I : S = struct let v = `a let f _ = v end At least now the interpreter doesn't complain. Many thanks ! Philippe. > > Jacques Garrigue > --0016e68e91964686e2048694a0ab Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

2010/5/14 Jacques Garrigue <= garrigue@math.nagoya-u.ac.jp>
From: Philippe Veber <philippe.veber@googlemail.com>

> I'd like to define a type with a variable that is constrained to a= ccept only
> polymorphic variant types included in a given set of tags. That is how= I
> believed one should do :
>
> =A0 =A0 =A0 =A0 Objective Caml version 3.11.2
>
> # type 'a t =3D 'a constraint 'a =3D [< `a | `b ];;
> type 'a t =3D 'a constraint 'a =3D [< `a | `b ]
>
> But I stumbled upon the following problem, when trying to use this
> definition
>
>
> # module type S =3D sig
> =A0 val v : 'a t
> end;;
> module type S =3D sig val v : [< `a | `b ] t end
>
> # module I : S =3D struct
> =A0 =A0 let v =3D `a
> =A0 end;;
>
> =A0 Error: Signature mismatch:
> =A0 =A0 =A0 =A0Modules do not match: sig val v : [> `a ] end is not= included in S
> =A0 =A0 =A0 =A0Values do not match:
> =A0 =A0 =A0 =A0 =A0val v : [> `a ]
> =A0 =A0 =A0 =A0is not included in
> =A0 =A0 =A0 =A0 =A0val v : [< `a | `b ] t
>
> Does anyone know why the definition of module I is rejected ? And if t= his is
> the intended behavior, why does the following work ?
>
> # let v : 'a t =3D `a
> =A0 ;;
> val v : [< `a | `b > `a ] t =3D `a

But it doesn't really work!
More precisely, the type [< `a | `b > `a ] t is an instance of 'a= t,
not 'a t itself, an a module interface should give a type at most as general as the implementation.

Right, I understand= now there are two different mechanisms at hand here : in the module case, = the type annotation for v is a specification, in the let binding case, it i= s a constraint. Seems like my question was better suited to beginners list = ! Just to be sure : module I is rejected because v should have type 'a = t for all 'a satisfying the constraint 'a =3D [< `a | `b ], that= contain in particular [ `b ], which is incompatible with the type of v. Is= that correct ?

=A0

In your case, you should simply write

=A0type t =3D [`a | `b]

since you don't know what v may be.

If i absol= utely wanted to forbid other tags than `a and `b, while keeping the possibi= lity to manage subtype hierarchies, maybe I could also change the code this= way :

type u =3D [`a | `b]
type 'a t =3D 'a constraint 'a =3D = [< u ]

module type S =3D sig
=A0 val v : u t
=A0 val f : &#= 39;a t -> [`a] t
end

module I : S =3D struct
=A0 let v =3D = `a
=A0 let f _ =3D v
end

At least now the interpreter doesn't complain. Many thanks !=

Philippe.

=A0

Jacques Garrigue

--0016e68e91964686e2048694a0ab--