Typing problems when using LablGTK

Typing problems when using LablGTK

[Mattias Waldau]

The first program works fine, but if I take the let button-part and move it to a separate
function called mini, the compilation fails. The type of the method attach is different.

What have I misunderstood?

/mattias

P.s. I learning GNOME using the book "Beginning GTK+/GNOME Programming", and sometimes it is
difficult to map GTK in C to LablGTK. I am on page 111.

Program 1, works.
=================

open GMain

let main () =
  let window = GWindow.window ~border_width:10 ~title:"Fun with tables" ~width:320 ~height:200 () in
  window#connect#destroy ~callback:Main.quit; 
  let table = GPack.table ~rows:10 ~columns:10 ~packing:window#add () in
  let button = GButton.button ~label:"test"
      ~packing:(table#attach ~left:2 ~top:2 ~expand:`BOTH) () in
(*  mini table; *)
  window#show ();
  Main.main ()

let _ = Printexc.print main ()


Program 2, fails
================

open GMain

let mini table : unit =
  GButton.button ~label:"mini"
    ~packing:(table#attach ~left:3 ~top:3 ~expand:`BOTH) ();
  ()

  
let main () =
  let window = GWindow.window ~border_width:10 ~title:"Fun with tables" ~width:320 ~height:200 () in
  window#connect#destroy ~callback:Main.quit; 
  let table = GPack.table ~rows:10 ~columns:10 ~packing:window#add () in
  mini table; 
  window#show ();
  Main.main ()

let _ = Printexc.print main ()



        Objective Caml version 3.00+20 (2000-12-03)

#                                   Characters 366-371:
This expression has type
  GPack.table =
    < add : GObj.widget -> unit; as_widget : Gtk.widget Gtk.obj;
      attach : int ->
               int ->
               ?right:int ->
               ?bottom:int ->
               ?expand:Gtk.Tags.expand_type ->
               ?fill:Gtk.Tags.expand_type ->
               ?shrink:Gtk.Tags.expand_type ->
               ?xpadding:int -> ?ypadding:int -> GObj.widget -> unit;
      children : GObj.widget list; coerce : GObj.widget;
      connect : GContainer.container_signals; destroy : unit -> unit;
      drag : GObj.drag_ops; focus : GContainer.focus; get_id : int;
      misc : GObj.misc_ops; remove : GObj.widget -> unit;
      set_border_width : int -> unit; set_col_spacing : int -> int -> unit;
      set_col_spacings : int -> unit; set_homogeneous : bool -> unit;
      set_row_spacing : int -> int -> unit; set_row_spacings : int -> unit >
but is here used with type
  < add : GObj.widget -> unit; as_widget : Gtk.widget Gtk.obj;
    attach : int -> int -> [> `BOTH] -> GObj.widget -> unit;
    children : GObj.widget list; coerce : GObj.widget;
    connect : GContainer.container_signals; destroy : unit -> unit;
    drag : GObj.drag_ops; focus : GContainer.focus; get_id : int;
    misc : GObj.misc_ops; remove : GObj.widget -> unit;
    set_border_width : int -> unit; set_col_spacing : int -> int -> unit;
    set_col_spacings : int -> unit; set_homogeneous : bool -> unit;
    set_row_spacing : int -> int -> unit; set_row_spacings : int -> unit >
# 

Re: Typing problems when using LablGTK

[Maxence]

Just add explicit type for the table parameter of your mini function :

let mini (table : GPack.table) : unit =
  GButton.button ~label:"mini"
    ~packing:(table#attach ~left:3 ~top:3 ~expand:`BOTH) ();
  ()

> What have I misunderstood?
I think you didn't misunderstood anything. I was surprised too, the
first time :-)
take a look at the example below :
class context () =
  object
    method get_string ?(default="great!") message =
      (* this function could display a message and an
	 entry widget to make the user type in some text.
	 The entry would contain the default text when
	 the window appears. for the example, we
	 just return the default text.*)
      print_string message;
      default
  end

let f ctx = ctx#get_string "how do you feel ?"

let ctx = new context ()
let feeling = f (ctx :> <get_string : string -> string>)

ocaml complains about the coercion of ctx :
This expression cannot be coerced to type < get_string : string ->
string >;
it has type context = < get_string : ?default:string -> string -> string
>
but is here used with type < get_string : string -> string >

The question is : why is this coercion not allowed ?

Maxence Guesdon

Re: Typing problems when using LablGTK

[Jacques Garrigue]

Hello Mattias,

> The first program works fine, but if I take the let button-part and
> move it to a separate function called mini, the compilation fails.
> The type of the method attach is different.
> 
> What have I misunderstood?

Your problem is explained in the tutorial (1st part of the reference
manual) in section 2.1.3. To be correctly handled, labeled and
optionals arguments need to be known at the application point.  If you
move this application out of its context, the type information is
lost, and an incorrect type is inferred.

The standard solution is to add a type annotation on objects whose
methods have optional arguments:

let mini (table : GPack.table) =
  GButton.button ~label:"mini"
    ~packing:(table#attach ~left:3 ~top:3 ~expand:`BOTH) ();
  ()

> /mattias
> 
> P.s. I learning GNOME using the book "Beginning GTK+/GNOME
> Programming", and sometimes it is difficult to map GTK in C to
> LablGTK. I am on page 111.

While the relation is kept intuitive, there are indeed differences
between GTK and LablGTK. Otherwise you wouldn't be able to write much
shorter programs :-) If you really don't know how to translate, the
low-level interface gives access to the raw calls, but this is much
less comfortable.

> Program 2, fails
> ================
> 
> open GMain
> 
> let mini table : unit =
>   GButton.button ~label:"mini"
>     ~packing:(table#attach ~left:3 ~top:3 ~expand:`BOTH) ();
>   ()
> 
>   
> let main () =
>   let window = GWindow.window ~border_width:10 ~title:"Fun with tables" ~width:320 ~height:200 () in
>   window#connect#destroy ~callback:Main.quit; 
>   let table = GPack.table ~rows:10 ~columns:10 ~packing:window#add () in
>   mini table; 
>   window#show ();
>   Main.main ()
> 
> let _ = Printexc.print main ()

RE: Typing problems when using LablGTK

[Mattias Waldau]

I also noted that typing the argument solved the problem. 

But why can't the typechecking complain if there is more than one 
typing possible? The current algorithm seems to take the first
solution found and keep that. 

Couldn't it instead say, "Ambiguous typing"?

/mattias

RE: Typing problems when using LablGTK

[Jacques Garrigue]

From: "Mattias Waldau" <mattias.waldau@abc.se>

> I also noted that typing the argument solved the problem. 
> 
> But why can't the typechecking complain if there is more than one 
> typing possible? The current algorithm seems to take the first
> solution found and keep that. 

This is not a completely arbitrary solution. This is the solution that
would be choosen if there were no optional arguments in the language.
A better solution would require some kind of whole program analysis,
to see on which function mini is applied, a bit of an overkill for a
rather exceptional problem.

> Couldn't it instead say, "Ambiguous typing"?

Unfortunately, no. Since any function may have optional arguments, all
function calls are in essence ambiguous. Still, what is ambiguous is
only the typing, the semantics is defined independently of types, and
guaranteed to be the same with or without type annotations. The worst
thing that may happen is that your program wouldn't be accepted by the
type checker.

From: Maxence <max@sbuilders.com>

> let feeling = f (ctx :> <get_string : string -> string>)
> 
> ocaml complains about the coercion of ctx :
> This expression cannot be coerced to type < get_string : string ->
> string >;
> it has type context = < get_string : ?default:string -> string -> string
> >
> but is here used with type < get_string : string -> string >
> 
> The question is : why is this coercion not allowed ?

The question is : how do you compile it. Since ?default:string ->
string -> string and string -> string correspond to incompatible
internal representations, one would have to build a new class with the
expected type, and masquerade ctx as an object of this class. This
seems to be too much work and too costly for something that can be
solved by a single type annotation.

The only case in which such a conversion is currently done is when you
pass a function with optional arguments as parameter to another
function.
     let button = GButton.button ~packing:(vbox#pack ~from:`END) ()
packing has type (widget -> unit) but vbox#pack has type
  ?from:Gtk.Tags.pack_type -> ?expand:bool ->
  ?fill:bool -> ?padding:int -> widget -> unit
meaning that some optional parameters are left after the partial
application. Currently the compiler discards them, by eta-expanding
the argument. But even this can subtly break the semantics in classic
mode (not in a fundamental way, but this is a petty headache).

Jacques Garrigue
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>