From mboxrd@z Thu Jan 1 00:00:00 1970 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 q2L8M44v017997 for ; Wed, 21 Mar 2012 09:22:04 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0EAJqOaU+FBoIF/2dsb2JhbABEuASCCQEBBAEnEwYDATUBAQMLCzQSVwaIGASkToQzjlEBBpAeY4hYjQuQJ4J2 X-IronPort-AV: E=Sophos;i="4.73,621,1325458800"; d="scan'208";a="150479504" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 21 Mar 2012 09:21:58 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 062DC62B4; Wed, 21 Mar 2012 17:21:56 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id CB25B40C3; Wed, 21 Mar 2012 17:21:55 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=Pvfby67dammtgiVrOd3EtOsoMHs=; b=yvJeL4SZb8hvWMl5XapilE2NlzS1 y6R447/OlmjsIWaYNJ9Zq9/qBbYjfibNWWOp8XI1uVOzyZQqs/vDnTWV1mwW/Xh1 njKrqq8x6T6NN44XSU/5HFhSnBzdNWxmhr3Mp0NVMPPMbFyNguLbB7ZlGICYp5yr dJd5z0PZEkr7vzQ= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=2WyxIR6wIfKfsv+gWcd1Z5qW4OWlMg1jokKmdlb5MYv3VLFFz+ow9bREncjWiPTjmR+m5anl/8lWtmpR7MGbwsUJ3WAsbBfzqL8X7uSdRVscJqk1v5JTNS+LSF2jIPo8bfBNH/ZCy21PxBM96s77TwfuS61wTWqOyZEJ2mieDEc=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 795CD3974; Wed, 21 Mar 2012 17:21:55 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Wed, 21 Mar 2012 17:21:55 +0900 Cc: caml users Message-Id: <3EB8D30A-FB02-4654-9F95-B7FF029F02FE@math.nagoya-u.ac.jp> References: To: Philippe Veber X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q2L8M44v017997 Subject: Re: [Caml-list] Explicitely named type variable and type constraints. On 2012/03/21, at 16:48, Philippe Veber wrote: > 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) Indeed, this is clearly wrong: these two module types are not equivalent. > 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 Wrong again, as subtyping between module signatures does not allow free type variables. > 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). No, currently there is no way to do that. One can only create locally abstract types, not locally private types. In theory I see no problem doing that, but with the current approach this would require new syntax, and be rather heavy. let f (type s = private [> `quit]) (screen : s screen) = ... And to be fully general, recursion between those types should be allowed too... As a side note, writing type message = private [> unit] makes the problem clearer. And solves it in some cases: module type Screen = sig type state type message = private [> `quit ] val init : state val emit : state -> message option end # let f (module Screen : Screen) = match Screen.(emit init) with | Some `quit -> 1 | _ -> 0 ;; val f : (module Screen) -> int = (using 4.00, but you can also write with (val ...)) Jacques Garrigue