[Caml-list] type inference with classes

[Caml-list] type inference with classes

[Ivan]

[-- Attachment #1: Type: text/plain, Size: 931 bytes --]

Hi!

I've mentioned that in some cases ocaml can't infer type (or maybe it can,
but didn't want to...) of some objects.
Right to this moment, I've just do as ocaml wants - annotate a type and
move forward. But now I want to make things more consciously. The reason is
simple - sometimes ocaml infers types correctly and denotes a type error in
my code, but I, mistakenly thinking that it can't infer type of object,
loose my time in useless type annotating of different identifiers. Or vice
versa, the code is correct, except for some undecidable object type, and I
spend h^Wminutes in checking my code for errors.

So, I'would like to know the rules of type inference failures with object
types. In what cases an object type can and must be inferred, and in what
it must be annotated explicitly?

Can someone share this arcane knowledge or, at least, point me at some
sources, explaining this issue?

Thanks everybody in advance!

[-- Attachment #2: Type: text/html, Size: 1072 bytes --]

Re: [Caml-list] type inference with classes

[Alain Frisch]

Hello,

I don't know if this covers all the case, but you need to keep in mind 
the following points.  Feel free to add to the list.

1. The type-checker will never infer that a method is polymorphic.  You 
need to tell it.

  object(this)
     method f = (this # g 1, this # g true)
     method g x = x
  end

===>

   object(this)
     method f = (this # g 1, this # g true)
     method g: 'a. 'a -> 'a = fun x -> x
   end


2. Same for labeled and optional arguments on methods, when the type for 
the method to be called is not known.

   class virtual c =
     object(this)
       method f = this # g ~x:1 ~y:2 + this # g ~y:1 ~x:2
     end

===>

   class virtual c =
     object(this)
       method f = this # g ~x:1 ~y:2 + this # g ~y:1 ~x:2
       method virtual g: x:int -> y:int -> int
     end

(Note: this is really not specific to objects, a simple (fun g -> g ~x:1 
~y:2 + g ~y:1 ~x:2) has the same effect, but it's likely to hit you if 
you use virtual classes.)

3. When declaring classes, the inferred type must have no free variable. 
  So while the expression "object method f x = x end" is allowed and is 
inferred to have a type "< f : 'a -> 'a >", the following class 
declaration is rejected:

class c = object method f x = x end

Depending on what you want to do, you can either force a specific type 
or make the class parametric:

class c = object method f x : int = x end
class ['a] c = object method f x : 'a = x end


-- Alain




On 8/3/2012 6:23 AM, Ivan wrote:
> Hi!
>
> I've mentioned that in some cases ocaml can't infer type (or maybe it
> can, but didn't want to...) of some objects.
> Right to this moment, I've just do as ocaml wants - annotate a type and
> move forward. But now I want to make things more consciously. The reason
> is simple - sometimes ocaml infers types correctly and denotes a type
> error in my code, but I, mistakenly thinking that it can't infer type of
> object, loose my time in useless type annotating of different
> identifiers. Or vice versa, the code is correct, except for some
> undecidable object type, and I spend h^Wminutes in checking my code for
> errors.
>
> So, I'would like to know the rules of type inference failures with
> object types. In what cases an object type can and must be inferred, and
> in what it must be annotated explicitly?
>
> Can someone share this arcane knowledge or, at least, point me at some
> sources, explaining this issue?
>
> Thanks everybody in advance!

Re: [Caml-list] type inference with classes

[Ivan]

[-- Attachment #1: Type: text/plain, Size: 1726 bytes --]

On 3 August 2012 08:50, Alain Frisch <alain@frisch.fr> wrote:

> Hello,
>
> I don't know if this covers all the case, but you need to keep in mind the
> following points.  Feel free to add to the list.
>

Thanks for nice and structured answer!

I'll try to expand it with my cases, but due to lack of comprehension they
will not be so clear =)

So the setup is follows: I have a class with a type explicitly specified in
mli file. No inference on it's methods. And a function, that takes some
object and type system tries to infer what objects it can accept.

Starting from a  simple case:

let reset_env_model state v =
  let q = Queue.create () in
  Queue.iter (fun p -> v#expand_row p) q

produces an error:
    This expression has type GTree.view
       but an expression was expected of type < expand_row : 'a -> unit; ..
>
       Types for method expand_row are incompatible

because expand_row method of type GTree.view has type:
   expand_row : Gtk.tree_path -> unit;

I think, that compiler have a reason to refuse this code: function wants a
method, that can take an arbitrary value of type 'a, but I pass a method
that has a covariant type Gtk.tree_path in position left to arrow. So he
complains correctly. I agree =) I think that this case has
some correspondence with your  case #1.

But, why in the following code:

let reset_env_model state v =
  let q = Queue.create () in
  let m,_,_ = State.env_model state in
  m#foreach (fun p _ -> if v#row_expanded p then Queue.push p q; false);
  set_env_model state v;
  Queue.iter (fun p -> v#expand_row p) q

compiler cannot infer, that object p has type Gtk.tree_path, and with this
proposition imply, that the expand_row method has a type "Gtk.tree_path ->
unit"?

[-- Attachment #2: Type: text/html, Size: 2578 bytes --]

Re: [Caml-list] type inference with classes

[Jacques Garrigue]

On 2012/08/03, at 7:15, Ivan wrote:

> On 3 August 2012 08:50, Alain Frisch <alain@frisch.fr> wrote:
> Hello,
> 
> I don't know if this covers all the case, but you need to keep in mind the following points.  Feel free to add to the list.
> 
> Thanks for nice and structured answer! 
> 
> I'll try to expand it with my cases, but due to lack of comprehension they will not be so clear =)
> 
> So the setup is follows: I have a class with a type explicitly specified in mli file. No inference on it's methods. And a function, that takes some object and type system tries to infer what objects it can accept. 
> 
> Starting from a  simple case:
> 
> let reset_env_model state v =
>   let q = Queue.create () in
>   Queue.iter (fun p -> v#expand_row p) q
> 
> produces an error:
>     This expression has type GTree.view
>        but an expression was expected of type < expand_row : 'a -> unit; .. >
>        Types for method expand_row are incompatible
> 
> because expand_row method of type GTree.view has type:
>    expand_row : Gtk.tree_path -> unit;

> I think, that compiler have a reason to refuse this code: function wants a method, that can take an arbitrary value of type 'a, but I pass a method that has a covariant type Gtk.tree_path in position left to arrow. So he complains correctly. I agree =) I think that this case has some correspondence with your  case #1.


Your assumption is wrong. A function never "requires" polymorphism from an argument.
It may require a polymorphic method, but only if the type of this argument is given explicitly.

The fact is that, at least in lablgtk-2.14.2 (the current version), the type is

      expand_row : ?all:bool -> Gtk.tree_path -> unit

So this enters the second category of methods with optional arguments.

> But, why in the following code:
> 
> let reset_env_model state v =
>   let q = Queue.create () in
>   let m,_,_ = State.env_model state in
>   m#foreach (fun p _ -> if v#row_expanded p then Queue.push p q; false);
>   set_env_model state v;
>   Queue.iter (fun p -> v#expand_row p) q
> 
> compiler cannot infer, that object p has type Gtk.tree_path, and with this proposition imply, that the expand_row method has a type "Gtk.tree_path -> unit"? 


This is exactly the same problem as above.

In some situations it may be a good idea to use the -principal flag, to get more regular behavior from the type checker with respect to required type annotations.

	Jacques Garrigue

Re: [Caml-list] type inference with classes

[Ivan]

[-- Attachment #1: Type: text/plain, Size: 1053 bytes --]

On 3 August 2012 09:32, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>wrote:
>
> Your assumption is wrong. A function never "requires" polymorphism from an
> argument.
> It may require a polymorphic method, but only if the type of this argument
> is given explicitly.
>

Well, yes. I do not know what do you mean by saying "requiring
polymorphism", but I do agree that my reasoning was wrong.
Taking a simple example (without any classes):

# let rec f x y = x y;;
val f : ('a -> 'b) -> 'a -> 'b = <fun>

I see, that function really requires as it's first argument any unary
function. That is, from type scheme 'a -> 'b I can construct any type that
contains one and only one arrow. And there is no subtype polymorphism
 involved here. Correct me if I'm wrong.

The fact is that, at least in lablgtk-2.14.2 (the current version), the
> type is
>
>       expand_row : ?all:bool -> Gtk.tree_path -> unit
>
The first thing I've tried was specifying explicitly argument ~all. But
compiler refused to accept this too, with exactly the same error message...

[-- Attachment #2: Type: text/html, Size: 1672 bytes --]

RE: [Caml-list] type inference with classes

[Jacques Garrigue]

From: Ivan <ivg@ieee.org>
>>The fact is that, at least in lablgtk-2.14.2 (the current version), the
>> type is
>>
>>       expand_row : ?all:bool -> Gtk.tree_path -> unit

>The first thing I've tried was specifying explicitly argument ~all. But
>compiler refused to accept this too, with exactly the same error message...

For the ~all argument to be properly processed, you first need the
type of the method to be known.
The best solution is to put a type annotation on v.
The next solution is to pass an explicit optional argument:

	v#expand_row ?all:None x

I don't like it much because parameter order matters.

Jacques