Problem correlating input and output type

Problem correlating input and output type

[Goswin von Brederlow]

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

Re: [Caml-list] Problem correlating input and output type

[Tiphaine Turpin]

Goswin von Brederlow a écrit :
> Hi,
>
> last night I had a crazy idea
Definitely :-).

> [...]
>
>
> Can anyone think of a way to express this so that the type system keeps
> track of which callbacks are already connected?
>   
Here is an attempt (with only two "events"). Note that :
- the imperative version cannot prevent connecting a signal more than once
- such types can only represent sets of "parallel" edges of a lattice,
i.e., this doesn't generalises to arbitrary "typestate" properties
- this is just a curiosity, and not a reasonable way of doing such
things. Runtime checking would be much easier (but still a bit hackish).

Tiphaine

module LatticeFun : sig

  type ('foo, 'bar) r
  type t and f

  val make : unit -> (f, f) r
  val set_foo : (f, 'bar) r -> (t, 'bar) r
  val set_bar : ('foo, f) r -> ('foo, t) r
  val use : (t, t) r -> unit

end = struct

  type ('foo, 'bar) r = {foo : bool ; bar : bool}

  type t
  type f = t

  let make () = {foo = false ; bar = false}
  let set_foo x = {x with foo = true}
  let set_bar x = {x with bar = true}
  let use _ = ()

end

module LatticeImp : sig

  type ('foo, 'bar) r
  type t and f

  val make : unit -> (f, f) r
  val set_foo : ('foo, 'bar) r -> (t, 'bar) r
  val set_bar : ('foo, 'bar) r -> ('foo, t) r
  val use : (t, t) r -> unit

end = struct

  (* for some reason, the direct declaration causes a module type error *)
  type r1 = {mutable foo : bool ; mutable bar : bool}
  type ('foo, 'bar) r = r1

  type t
  type f = t

  let make () = {foo = false ; bar = false}
  let set_foo x = x.foo <- true ; x
  let set_bar x = x.bar <- true ; x
  let use _ = ()

end

Re: [Caml-list] Problem correlating input and output type

[Goswin von Brederlow]

Tiphaine Turpin <Tiphaine.Turpin@irisa.fr> writes:

> Goswin von Brederlow a écrit :
>> Hi,
>>
>> last night I had a crazy idea
> Definitely :-).
>
>> [...]
>>
>>
>> Can anyone think of a way to express this so that the type system keeps
>> track of which callbacks are already connected?
>>   
> Here is an attempt (with only two "events"). Note that :
> - the imperative version cannot prevent connecting a signal more than once
> - such types can only represent sets of "parallel" edges of a lattice,
> i.e., this doesn't generalises to arbitrary "typestate" properties
> - this is just a curiosity, and not a reasonable way of doing such
> things. Runtime checking would be much easier (but still a bit hackish).

But runtime checks will only show the error when the GUI object is
instantiated. Some obscure dialog might not pop up in month.

> Tiphaine
>
> module LatticeFun : sig
>
>   type ('foo, 'bar) r
>   type t and f
>
>   val make : unit -> (f, f) r
>   val set_foo : (f, 'bar) r -> (t, 'bar) r
>   val set_bar : ('foo, f) r -> ('foo, t) r
>   val use : (t, t) r -> unit
>
> end = struct
>
>   type ('foo, 'bar) r = {foo : bool ; bar : bool}
>
>   type t
>   type f = t
>
>   let make () = {foo = false ; bar = false}
>   let set_foo x = {x with foo = true}
>   let set_bar x = {x with bar = true}
>   let use _ = ()
>
> end
>
> module LatticeImp : sig
>
>   type ('foo, 'bar) r
>   type t and f
>
>   val make : unit -> (f, f) r
>   val set_foo : ('foo, 'bar) r -> (t, 'bar) r
>   val set_bar : ('foo, 'bar) r -> ('foo, t) r
>   val use : (t, t) r -> unit
>
> end = struct
>
>   (* for some reason, the direct declaration causes a module type error *)
>   type r1 = {mutable foo : bool ; mutable bar : bool}
>   type ('foo, 'bar) r = r1
>
>   type t
>   type f = t
>
>   let make () = {foo = false ; bar = false}
>   let set_foo x = x.foo <- true ; x
>   let set_bar x = x.bar <- true ; x
>   let use _ = ()
>
> end

Thanks. That solves the first problem. But how do you translate that
into ocaml objects?

type need_click
type have_click

class type ['click] clickable_type = object
  method set_click : ...?
  method use : ...?
end

I believe a method can not change the type of a class nor can it require
the parametereized class to be of a certain type. And if I write helper
function outside the class like

let set_foo x = x#foo <- true ; x

then I can't use inheritance for them. Maybe I can use inheritance
for the class objects and module inclusion for the set_* helpers. But
how do I write the use function so that one can not use of an inherited
class?

Or how do I specify

method add_connected_obj : (<connected>) obj

The <connected> would need to be specific to the exact type of object
being added. I do believe I need something that simplifies the type with
each aplication of a callback so that all fully connected objects will
have the same basic type, e.g.

unit need_click need_drag obj => unit need_click obj => unit obj

MfG
        Goswin

Re: [Caml-list] Problem correlating input and output type

[Tiphaine Turpin]

Goswin von Brederlow a écrit :
> Tiphaine Turpin <Tiphaine.Turpin@irisa.fr> writes:
>
>   
>> Goswin von Brederlow a écrit :
>>     
>>> [...]
>>>
>>> Can anyone think of a way to express this so that the type system keeps
>>> track of which callbacks are already connected?
>>>   
>> Runtime checking would be much easier (but still a bit hackish).
>>     
>
> But runtime checks will only show the error when the GUI object is
> instantiated. Some obscure dialog might not pop up in month.
[...]
> But how do you translate that into ocaml objects?
>
>   
I see two requirements in your problem that are difficult to combine:
- static checking by an "ordinary" type system
- dynamic connection of objects.

First, I believe that it prevents anything imperative (because such
typing ignores the execution flow). A functional approach may succeed in
some sense, but I don't think that it would be practical. As for the
combination with objects, In my (humble) experience with objects in
Ocaml, I found that typing even reasonably simple designs is not a
trivial task. So, combining that with the earlier hack would quickly
become a nightmare.

My personal opinion would be to drop the second condition, and make the
connection of your objects static. I would try to define the objects as
functors, with one module parameter per connection, and connect all that
using (possibly recursive) module definitions.

I'm curious to know what solutions object-oriented people could propose,
in particular with dependency injection.

Tiphaine