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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id BCF03BBAF for ; Mon, 17 May 2010 13:56:55 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: As8CACzM8EvRVda2mWdsb2JhbACdeAgVAQEBAQEICwoHESKtQQEFjVsBBIUQj0A X-IronPort-AV: E=Sophos;i="4.53,247,1272837600"; d="scan'208";a="59483984" Received: from mail-iw0-f182.google.com ([209.85.214.182]) by mail1-smtp-roc.national.inria.fr with ESMTP; 17 May 2010 13:56:54 +0200 Received: by iwn42 with SMTP id 42so310821iwn.27 for ; Mon, 17 May 2010 04:56:54 -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=AY4f/r/gAM32L7U1u8cMoNsFBgHuo20P3t/2k+z/Vk4=; b=bdwgACLf7khzShIbTXgJWYw4b+7DDbYkqaDQrCD37Kz+ofhHk46Slx/F79HDeIAuPm rhZt2fHM2vCl4MwUZ/mxLzqIJ2fe+ahQF5TaTZ19AoA/LbDDOW2K0fwBCgv861FlsY40 FDKfXHS5BgXtnRSXbV61dJdmhesV+QbZS70QY= 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=BaSnG2EPEDYMVRFngAX/mXjQH32HvUGIv45LNe0Z9ijoN2hrkFew1HU96CoRQhFKEf 0/Tx9QUaewvLVD6KNN41SZvjIfWHQftT/rXIgMIpC+ILj117E5Hsl/4vMZcgSZ8Owqba SPCZoynjB6+FGXDRtr/hZfFykcv+aKeVAJXcM= Received: by 10.231.177.133 with SMTP id bi5mr241943ibb.83.1274097414132; Mon, 17 May 2010 04:56:54 -0700 (PDT) MIME-Version: 1.0 Received: by 10.231.119.163 with HTTP; Mon, 17 May 2010 04:56:34 -0700 (PDT) In-Reply-To: <20100515.095445.134122748.garrigue@math.nagoya-u.ac.jp> References: <20100515.004940.200940107.garrigue@math.nagoya-u.ac.jp> <20100515.095445.134122748.garrigue@math.nagoya-u.ac.jp> From: Philippe Veber Date: Mon, 17 May 2010 13:56:34 +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=0016e64f5e8fc752da0486c8eb9d X-Spam: no; 0.00; variants:01 val:01 subtype:01 sig:01 val:01 struct:01 sig:01 subtype:01 struct:01 polymorphic:01 polymorphic:01 beginners:01 beginners:01 clearer:01 clearer:01 --0016e64f5e8fc752da0486c8eb9d Content-Type: text/plain; charset=ISO-8859-1 2010/5/15 Jacques Garrigue > From: Philippe Veber > > 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 : > ... > >> > 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 ? > > Yes, this is exactly the point I was trying to make. But it was a good > idea to post it here: this is a rather technical point, I don't read > the beginner-list usually, and your explanation is probably better > than mine. > > >> 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 ! > > This indeed works, but I'm not sure of why you insist on defining a > constrained type. What is wrong with writing directly the following? > > module type S = sig > val v : u > val f : [< u] -> [`a] > end > Well, nothing ! I'm affraid I chose an inappropriate solution to an irrelevant problem. Initially i just wanted to be sure my polymorphic type 'a t would not be used with funny tags in 'a (I mean tags that have nothing to do with t). But after all, there is (in my case) no rationale for this. Second, types may be shorter to write : val f : 'a t -> int instead of val f : [< u] t -> int or val f : [< My_type.u ] My_type.t -> int if in another module. Well, now it's clearer for me it was not such a smart idea. Your proposal is simpler and more natural. > Constrained types have their uses, which are, in brief ? Now I can't see a typical use for closed polymorphic variant types (I mean types of the form 'a t constraint 'a = [< ... ]) but I find them often confusing as > the type variable you write is not really a type variable. > why isn't it the case ? Aren't they simply type variables restricted to a finite number of types ? Anyway, thanks a lot for commenting on my problem ! Philippe. > Question of taste. > > Jacques Garrigue > --0016e64f5e8fc752da0486c8eb9d Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

2010/5/15 Jacques Garrigue <garrigue@math.nago= ya-u.ac.jp>
From: Philippe Veber <philippe.veber@googlemail.com>
> 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 constra= ined to accept
>> only
>> > polymorphic variant types included in a given set of tags. Th= at is how I
>> > believed one should do :
...
>> > Does anyone know why the definition of modu= le I is rejected ? And if this
>> 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 m= ost as
>> general as the implementation.
>>
>
> Right, I understand now there are two different mechanisms at hand her= e : 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 su= ited
> to beginners list ! Just to be sure : module I is rejected because v s= hould
> 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 ?

Yes, this is exactly the point I was trying to make. But it was a goo= d
idea to post it here: this is a rather technical point, I don't read the beginner-list usually, and your explanation is probably better
than mine.

>> In your case, you should simply write
>>
>> =A0type t =3D [`a | `b]
>>
>> since you don't know what v may be.
>>
>
> If i absolutely wanted to forbid other tags than `a and `b, while keep= ing
> the possibility to manage subtype hierarchies, maybe I could also chan= ge 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 : '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 !

This indeed works, but I'm not sure of why you insist on defining= a
constrained type. What is wrong with writing directly the following?

module type S =3D sig
=A0val v : u
=A0val f : [< u] -> [`a]
end
Well, nothing ! I'm affraid I chose an inappro= priate solution to an irrelevant problem. Initially i just wanted to be sur= e my polymorphic type 'a t would not be used with funny tags in 'a = (I mean tags that have nothing to do with t). But after all, there is (in m= y case) no rationale for this. Second, types may be shorter to write :

val f : 'a t -> int

instead of

val f : [< u] t = -> int

or

val f : [< My_type.u ] My_type.t -> int
if in another module. Well, now it's clearer for me it was not su= ch a smart idea. Your proposal is simpler and more natural.



Constrained types have their uses,
which are, in brief ? = Now I can't see a typical use for closed polymorphic variant types (I m= ean types of the form 'a t constraint 'a =3D [< ... ])

but I find = them often confusing as
the type variable you write is not really a type variable.
=
why isn't it the case ? Aren't they simply type variables rest= ricted to a finite number of types ?

Anyway, thanks a lot for commen= ting on my problem !

Philippe.




=A0
Question of taste.

Jacques Garrigue

--0016e64f5e8fc752da0486c8eb9d--