Problem correlating input and output type

[Goswin von Brederlow <goswin-v-b@web.de>]

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 = <fun>

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 = <fun>

# 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 = <fun>

# 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 = <fun>

# 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 = <fun>
val set_bla : (bla:bool -> 'a) -> 'a = <fun>
val set_bar : (bar:bool -> 'a) -> 'a = <fun>

# set_foo make;;
- : bla:bool -> bar:bool -> t = <fun>

# set_bar (set_bla (set_foo make));;
- : t = {foo = true; bla = true; bar = true}

# make ~bla:true;;
- : foo:bool -> bar:bool -> t = <fun>

# (make ~bla:true) ~bar:true;;
- : foo:bool -> t = <fun>

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