From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2L7mYdv016144 for ; Wed, 21 Mar 2012 08:48:34 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmYBAJWHaU9KfVK2kGdsb2JhbABDtnUIIgEBAQEJCQ0HFAQjgiICExkBGx4DEhBdAREBBQEiNYdolwGCXQqME4JxhSQ/iHYBBQuQdgSVX45IPYQK X-IronPort-AV: E=Sophos;i="4.73,621,1325458800"; d="scan'208";a="150474397" Received: from mail-we0-f182.google.com ([74.125.82.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 21 Mar 2012 08:48:29 +0100 Received: by wern13 with SMTP id n13so1181849wer.27 for ; Wed, 21 Mar 2012 00:48:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=ua3hMCT2Owell8mXa+hKEEXQ0OCTPmmcwRXXVnRKTA4=; b=EpdZJTI7s9eNN3AVYSyCJbqQViWAHO4DGoAXVCZNgX/CWxEhFB0GdYnAfIug4EpVW/ morRNa71nMsFD3T8wnFSogVlz8JvPzYdj8pp7fwhWgr6RLNJ4i+jZ+ZihRKcAJEicKpK z16YHpQMUcWNRjz/X0ih1sQw0Y4frRGbbSQLtEesd0ApFfsVZJPmra7lZ9XrQTIs2LKY vIj70tuX89U0txP+rN9wYYiuT5KppWvyzsfYd21wqHwcBUlnMppy5VuaCekX62Z1KCQi Bs9COC3PfMTX1rJKob0EkGVCH2hL6rpN9PkIBUtk/IFLynraDz2RW2VgtD64yb52YuMH 3dXw== Received: by 10.216.145.209 with SMTP id p59mr1690955wej.50.1332316109185; Wed, 21 Mar 2012 00:48:29 -0700 (PDT) MIME-Version: 1.0 Received: by 10.180.126.68 with HTTP; Wed, 21 Mar 2012 00:48:09 -0700 (PDT) From: Philippe Veber Date: Wed, 21 Mar 2012 08:48:09 +0100 Message-ID: To: caml users Content-Type: multipart/alternative; boundary=0016e6dee8306aa23604bbbc04be X-Validation-by: philippe.veber@gmail.com Subject: [Caml-list] Explicitely named type variable and type constraints. --0016e6dee8306aa23604bbbc04be Content-Type: text/plain; charset=ISO-8859-1 Hi, I found myself defining a type that would both contain a module type and a type constraint: module type Screen = sig type state type message val init : state [...] val emit : state -> message option end type 'a screen = (module Screen with type message = 'a) constraint 'a = [> `quit] That is supposed to express that screens emit messages, and that one of the messages can be "quit". Now I've got some trouble when using the 'a screen type in a function that unpack the module it contains: let f (screen : 'a screen) = let module Screen = (val *screen* : Screen) in match Screen.(emit init) with | Some `quit -> 1 | _ -> 0 ;; Error: This expression has type ([> `quit ] as 'a) screen = (module Screen with type message = 'a) but an expression was expected of type (module Screen) New attempt: # let f (screen : 'a screen) = let module Screen = (val screen : Screen with type message = 'a) in match Screen.(emit init) with | Some `quit -> 1 | _ -> 0 ;; Error: Unbound type parameter 'a Though here I'm not sure the error is right. New attempt: # let f (type s) (screen : s screen) = let module Screen = (val screen : Screen with type message = s) in match Screen.(emit init) with | Some `quit -> 1 | _ -> 0 ;; Error: This type s should be an instance of type [> `quit ] Which makes sense. So here is my question: is there a way to impose a constraint on the "newtype" introduced in argument? Let me say that I'm aware I should write this more simply. For instance in the module type Screen, emit could have type state -> [`quit | `message of message]. So my question is only a matter of curiosity. Still, I'd be happy to know :o). Cheers, Philippe. --0016e6dee8306aa23604bbbc04be Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hi,

I found myself defining a type that would both contain a module = type and a type constraint:

=A0 module type Screen =3D sig
=A0=A0=A0 type state
=A0=A0=A0 type message
=A0=A0=A0 val init : state
=A0 =A0 [...]
=A0=A0 val emit : state -> message option
=A0 end
=A0 type 'a screen =3D (module Screen with type message = =3D 'a) constraint 'a =3D [> `quit]

That is supposed to express that screens emit messages, and that one of= the messages can be "quit". Now I've got some trouble when u= sing the 'a screen type in a function that unpack the module it contain= s:

=A0 let f (screen : &= #39;a screen) =3D
=A0=A0=A0 let module Screen= =3D (val screen<= span style=3D"font-family:courier new,monospace"> : Screen) in
=A0=A0=A0 match Screen.(e= mit init) with
=A0=A0=A0=A0=A0 | Some `quit -&= gt; 1
=A0=A0=A0=A0=A0 | _ ->= 0
=A0=A0=A0
=A0 ;;
Error: This expression has type
=A0=A0=A0=A0=A0=A0=A0=A0 = ([> `quit ] as 'a) screen =3D (module Screen with type message =3D &= #39;a)
=A0=A0=A0=A0=A0=A0 but an expression wa= s expected of type (module Screen)

New attempt:

#= let f (screen : 'a screen) =3D
=A0=A0=A0= let module Screen =3D (val screen : Screen with type message =3D 'a) i= n
=A0=A0=A0 match Screen.(e= mit init) with
=A0=A0=A0=A0=A0 | Some `quit -&= gt; 1
=A0=A0=A0=A0=A0 | _ ->= 0
=A0
=A0 ;;
Error: Unbound type parameter 'a

Though here I'm not sure the error is right. New attempt:

# let f (type s) (scree= n : s screen) =3D
=A0=A0=A0 let module Screen= =3D (val screen : Screen with type message =3D s) in
=A0=A0=A0 match Screen.(e= mit init) with
=A0=A0=A0=A0=A0 | Some `quit -&= gt; 1
=A0=A0=A0=A0=A0 | _ ->= 0
=A0
=A0 ;;
Error: This type s should be an instance of type [> `quit ]

Which makes sense. So here is my question: is there a way to impose a c= onstraint on the "newtype" introduced in argument? Let me say tha= t I'm aware I should write this more simply. For instance in the module= type Screen, emit could have type state -> [`quit | `message of message= ]. So my question is only a matter of curiosity. Still, I'd be happy to= know :o).

Cheers,
=A0 Philippe.


--0016e6dee8306aa23604bbbc04be--