RE: Typing problems when using LablGTK

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

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>