From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 74A35BBAF for ; Sun, 31 Jan 2010 19:01:58 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApQBAO5TZUvZSMDjimdsb2JhbACBM5oPAQEBCgkMBxEFulaERQQ X-IronPort-AV: E=Sophos;i="4.49,378,1262559600"; d="scan'208";a="55023259" Received: from fmmailgate02.web.de ([217.72.192.227]) by mail4-smtp-sop.national.inria.fr with ESMTP; 31 Jan 2010 19:01:57 +0100 Received: from smtp08.web.de (fmsmtp08.dlan.cinetic.de [172.20.5.216]) by fmmailgate02.web.de (Postfix) with ESMTP id 194E014CE45F5 for ; Sun, 31 Jan 2010 19:01:57 +0100 (CET) Received: from [95.208.117.111] (helo=frosties.localdomain) by smtp08.web.de with asmtp (TLSv1:AES256-SHA:256) (WEB.DE 4.110 #314) id 1Nbe7Q-00042W-00 for caml-list@yquem.inria.fr; Sun, 31 Jan 2010 19:01:57 +0100 Received: from mrvn by frosties.localdomain with local (Exim 4.71) (envelope-from ) id 1Nbe7Q-0001YH-IB for caml-list@yquem.inria.fr; Sun, 31 Jan 2010 19:01:56 +0100 From: Goswin von Brederlow To: caml-list@yquem.inria.fr Subject: Problem correlating input and output type Date: Sun, 31 Jan 2010 19:01:56 +0100 Message-ID: <87fx5mi25n.fsf@frosties.localdomain> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: goswin-v-b@web.de X-Sender: goswin-v-b@web.de X-Provags-ID: V01U2FsdGVkX1+Dy3hyTOInkixmGKEF1qwF4eRUl4PAftbpeyub RFvDwfRW2HIVfo0nxr6A3ajwYWJH9c4r6YxqjzVDu4PHE0dm6f iIueV5EAg= X-Spam: no; 0.00; mutable:01 bool:01 variants:01 mutable:01 foo:01 bool:01 foo:01 val:01 unconnected:01 val:01 callbacks:01 totaly:98 mfg:98 polymorphic:01 polymorphic:01 Hi, last night I had a crazy idea for a better GUI framework. In a GUI you have objects that react to events (being clicked, being dragged, covered/uncovered, resized ...). Oftent basic objects (e.g. buttons) are then combined to build higher level objects (e.g. dialog boxes). Each object now has their own set of events that it handles internally and events that need to be reacted to by some callback. For example a dialog box redraws itself when resized. But clicking on "ok" needs to be handled outside the dialog box. If any event remains unanswered that is usualy a bad thing. You click at "ok" and nothing happens. Not good. Now my crazy idea was that the type of an object should include the events lacking a callback. I simplified this to a mutable bool that needs to be set true. Method 1: polymorphic variants ------------------------------ # type 'a t = { mutable foo : bool; mutable bla : bool; mutable bar : bool } let make () = ({ foo = false; bla = false; bar = false; } : [`Foo | `Bla | `Bar] t);; type 'a t = { mutable foo : bool; mutable bla : bool; mutable bar : bool; } val make : unit -> [ `Bar | `Bla | `Foo ] t = The make method gives a totaly unconnected object that still needs Foo, Bla and Bar set. # let (set_foo : [> `Foo ] t -> [> ] t) = function x -> x.foo <- true; x;; val set_foo : ([> `Foo ] as 'a) t -> 'a t = # set_foo (make ());; - : [ `Bar | `Bla | `Foo ] t = {foo = true; bla = false; bar = false} As you can see the type correlation that the output type no longer contains `Foo doesn't work. I would like the type to be like this: let (set_foo : [ `Foo | 'a ] t -> [ 'a ] t) = function x -> x.foo <- true; x;; Method 2: polymorphic types --------------------------- # type 'a foo type 'a bla type 'a bar type 'a t = { mutable foo : bool; mutable bla : bool; mutable bar : bool } let make () = ({ foo = false; bla = false; bar = false; } : unit foo bla bar t);; type 'a foo type 'a bla type 'a bar type 'a t = { mutable foo : bool; mutable bla : bool; mutable bar : bool; } val make : unit -> unit foo bla bar t = # let (set_foo : 'a foo 'b -> 'a 'b) = function x -> x.foo := true; x;; Unfortunately the 'b isn't allowed in that position. Method 3: labeled arguments --------------------------- # type t = { mutable foo : bool; mutable bla : bool; mutable bar : bool } let make ~foo ~bla ~bar = { foo = foo; bla = bla; bar = bar };; type t = { mutable foo : bool; mutable bla : bool; mutable bar : bool; } val make : foo:bool -> bla:bool -> bar:bool -> t = # let set_foo x = x ~foo:true let set_bla x = x ~bla:true let set_bar x = x ~bar:true;; val set_foo : (foo:bool -> 'a) -> 'a = val set_bla : (bla:bool -> 'a) -> 'a = val set_bar : (bar:bool -> 'a) -> 'a = # set_foo make;; - : bla:bool -> bar:bool -> t = # set_bar (set_bla (set_foo make));; - : t = {foo = true; bla = true; bar = true} # make ~bla:true;; - : foo:bool -> bar:bool -> t = # (make ~bla:true) ~bar:true;; - : foo:bool -> t = That looks good so far. BUT # set_bla make;; Error: This expression has type foo:bool -> bla:bool -> bar:bool -> t but an expression was expected of type bla:bool -> 'a While I can use the labeled in any order on the original function that does not translate to parameter passing. Can anyone think of a way to express this so that the type system keeps track of which callbacks are already connected? MfG Goswin