[Caml-list] Odd failure to infer types

[Caml-list] Odd failure to infer types

[Goswin von Brederlow]

Hi,

I'm implementing a solver for the game Atomix. If you don't know it then
don't worry. It isn't relevant.

I split things up into submodules and now one of the submodules does not
infere the right types:

File "Atomix.ml", line 168, characters 11-876:
Error: The type of this module,
       sig
         type dir = NORTH | SOUTH | WEST | EAST
         val max_moves : int
         val cache : (string, unit) Hashtbl.t
         val states :
           ('_a list * (char * int * int) array * string) list array
         val string_of_dir : dir -> string
         val print :
           (int * int * dir) list * (char * int * int) array * string -> unit
         val num_states : int
       end, contains type variables that cannot be generalized

I believe this is wrong. In S.num_states the call to "print state"
fixates the type for state and the "states.(d) <- state::states.(d);"
should then fixate the missing '_a in the type for states.

Anyone know why?

MfG
        Goswin

----------------------------------------------------------------------
module B = struct
  exception Outside
  let width = 14
  let height = 6
  let board = ""
    ^ "  #         # "
    ^ "  #         # "
    ^ "  #           "
    ^ "  # #  #######"
    ^ "    #         "
    ^ "    #         "

  let start =
    Array.of_list
      (List.sort compare
	 [
	   ('A',  1, 3); (*  H- *)
	   ('B', 10, 5); (* -O- *)
	   ('C', 13, 1); (* -H  *)
	 ])

  let get board x y =
    if (x < 0) || (x >= width) || (y < 0) || (y >= height)
    then '#'
    else board.[x + y * width]

  let set board x y c =
    if (x < 0) || (x >= width) || (y < 0) || (y >= height)
    then raise Outside;
    let board = String.copy board
    in
    board.[x + y * width] <- c;
    board

  let print board =
    Printf.printf "  ";
    for x = 0 to width - 1 do
      Printf.printf "%c" (char_of_int (int_of_char 'A' + x));
    done;
    Printf.printf "\n";
    Printf.printf " +--------------+\n";
    for y = 0 to height - 1 do
      Printf.printf "%d|" (y + 1);
      for x = 0 to width - 1 do
	Printf.printf "%c" board.[y * width + x];
      done;
      Printf.printf "|\n";
    done;
    Printf.printf " +--------------+\n";
    flush_all ()
end

module G = struct
  let width = 3
  let height = 1
  let atoms = "ABC"

  let get x y =
    if (x < 0) || (x >= width) || (y < 0) || (y >= height)
    then '~'
    else atoms.[x + y * width]
    
  let solutions =
    let rec loopy acc = function
      | -1 -> acc
      | y ->
	let rec loopx acc = function
	  | -1 -> loopy acc (y - 1)
	  | x ->
	    let rec loopv acc sol board = function
	      | -1 ->
		B.print board;
		let sol = Array.of_list (List.sort compare sol)
		in
		loopx ((sol, board)::acc) (x - 1)
	      | v ->
		let rec loopu acc sol board = function
		  | -1 -> loopv acc sol board (v - 1)
		  | u ->
		    let c = get u v
		    in
		    if c = ' '
		    then loopu acc sol board (u - 1)
		    else if B.get board (x + u) (y + v) = ' '
		    then
		      begin
			let board = B.set board (x + u) (y + v) c
			in
			loopu acc ((c, x + u, y + v)::sol) board (u - 1)
		      end
		    else loopx acc (x - 1) 
		in
		loopu acc sol board (width - 1)
	    in
	    loopv acc [] B.board (height - 1)
	in
	loopx acc (B.width - width)
    in
    loopy [] (B.height - height)

  let print (sol, board) =
    B.print board;
    Array.iter
      (fun (c, x, y) ->
	Printf.printf "%c: (%c, %d)\n" c
	  (char_of_int (int_of_char 'A' + x))
	  (y + 1))
      sol;
    flush_all ()
end

module D = struct
  let infty = 999999
  let make_one x y =
    let d = Array.make_matrix B.width B.height infty in
    let rec loop n acc = function
      | [] ->
	if acc = []
	then d
	else loop (n + 1) [] acc
      | (u, v)::xs ->
	let rec move acc x y dx dy =
	  if B.get B.board x y = ' '
	  then
	    let acc =
	      if d.(x).(y) > n
	      then
		begin
		  d.(x).(y) <- n;
		  (x, y)::acc
		end
	      else acc
	    in
	    move acc (x + dx) (y + dy) dx dy
	  else acc
	in
	let acc = move acc u v (-1) 0 in
	let acc = move acc u v 1 0 in
	let acc = move acc u v 0 (-1) in
	let acc = move acc u v 0 1
	in
	loop n acc xs
    in
    d.(x).(y) <- 0;
    loop 1 [] [(x, y)]

  let dist =
    Array.init B.width (fun x -> Array.init B.height (fun y -> make_one x y))

  let get x1 y1 x2 y2 =
    if (x1 < 0) || (x1 >= B.width) || (y2 < 0) || (y2 >= B.height)
      || (x2 < 0) || (x2 >= B.width) || (y2 < 0) || (y2 >= B.height)
    then infty
    else dist.(x1).(y1).(x2).(y2)

  let get_all pos =
    let d =
      Array.mapi
	(fun i (c, x1, y1) ->
	  let (_, x2, y2) = B.start.(i)
	  in
	  get x1 y1 x2 y2)
	pos
    in
    Array.fold_left ( + ) 0 d
end

module S = struct
  type dir = NORTH | SOUTH | WEST | EAST

  let max_moves = 1000
  let cache = Hashtbl.create 0
    (*
  let states = ((Array.make max_moves []) :
      ((int * int * dir) list * (char * int * int) array * string) list array)
    *)
  let states = Array.make max_moves []

  let string_of_dir = function
    | NORTH -> "norden"
    | SOUTH -> "sueden"
    | WEST -> "westen"
    | EAST -> "osten"
      
  let print (moves, (_ : (char * int * int) array), board) =
    B.print board;
    List.iter
      (fun (x, y, dir) ->
	Printf.printf "zug %c %d %s,"
	  (char_of_int (int_of_char 'A' + x))
	  (y + 1)
	  (string_of_dir dir))
      moves

  let num_states =
    List.fold_left
      (fun num (sol, board) ->
	let d = D.get_all sol in
	let state = ([], sol, board)
	in
	Hashtbl.add cache board ();
	states.(d) <- state::states.(d);
	print state;
	num + 1)
      0
      G.solutions
end

let () =
  List.iter G.print G.solutions;
  Printf.printf "%d solutions\n" (List.length G.solutions)

Re: [Caml-list] Odd failure to infer types

[Christophe Papazian]

The type of [] is 'a list. This is (strong) polymorphism. Calling a  
function 'int list -> ?' on [] doesn't not
remove the polymorphism of []. However, an '_a list array is not  
polymorphism, it's just the compiler who don't know
yet the type inside the lists. And as you give him [], he can't deduce  
the type.

As an example you can do this :

let s = [] in 1::s, 'a'::s, [|s|]	;;

And it still doesn't know...

Le 3 sept. 11 à 11:53, Goswin von Brederlow a écrit :

> Hi,
>
> I'm implementing a solver for the game Atomix. If you don't know it  
> then
> don't worry. It isn't relevant.
>
> I split things up into submodules and now one of the submodules does  
> not
> infere the right types:
>
> File "Atomix.ml", line 168, characters 11-876:
> Error: The type of this module,
>       sig
>         type dir = NORTH | SOUTH | WEST | EAST
>         val max_moves : int
>         val cache : (string, unit) Hashtbl.t
>         val states :
>           ('_a list * (char * int * int) array * string) list array
>         val string_of_dir : dir -> string
>         val print :
>           (int * int * dir) list * (char * int * int) array * string  
> -> unit
>         val num_states : int
>       end, contains type variables that cannot be generalized
>
> I believe this is wrong. In S.num_states the call to "print state"
> fixates the type for state and the "states.(d) <- state::states.(d);"
> should then fixate the missing '_a in the type for states.
>
> Anyone know why?
>
> MfG
>        Goswin
>
> ----------------------------------------------------------------------
> module B = struct
>  exception Outside
>  let width = 14
>  let height = 6
>  let board = ""
>    ^ "  #         # "
>    ^ "  #         # "
>    ^ "  #           "
>    ^ "  # #  #######"
>    ^ "    #         "
>    ^ "    #         "
>
>  let start =
>    Array.of_list
>      (List.sort compare
> 	 [
> 	   ('A',  1, 3); (*  H- *)
> 	   ('B', 10, 5); (* -O- *)
> 	   ('C', 13, 1); (* -H  *)
> 	 ])
>
>  let get board x y =
>    if (x < 0) || (x >= width) || (y < 0) || (y >= height)
>    then '#'
>    else board.[x + y * width]
>
>  let set board x y c =
>    if (x < 0) || (x >= width) || (y < 0) || (y >= height)
>    then raise Outside;
>    let board = String.copy board
>    in
>    board.[x + y * width] <- c;
>    board
>
>  let print board =
>    Printf.printf "  ";
>    for x = 0 to width - 1 do
>      Printf.printf "%c" (char_of_int (int_of_char 'A' + x));
>    done;
>    Printf.printf "\n";
>    Printf.printf " +--------------+\n";
>    for y = 0 to height - 1 do
>      Printf.printf "%d|" (y + 1);
>      for x = 0 to width - 1 do
> 	Printf.printf "%c" board.[y * width + x];
>      done;
>      Printf.printf "|\n";
>    done;
>    Printf.printf " +--------------+\n";
>    flush_all ()
> end
>
> module G = struct
>  let width = 3
>  let height = 1
>  let atoms = "ABC"
>
>  let get x y =
>    if (x < 0) || (x >= width) || (y < 0) || (y >= height)
>    then '~'
>    else atoms.[x + y * width]
>
>  let solutions =
>    let rec loopy acc = function
>      | -1 -> acc
>      | y ->
> 	let rec loopx acc = function
> 	  | -1 -> loopy acc (y - 1)
> 	  | x ->
> 	    let rec loopv acc sol board = function
> 	      | -1 ->
> 		B.print board;
> 		let sol = Array.of_list (List.sort compare sol)
> 		in
> 		loopx ((sol, board)::acc) (x - 1)
> 	      | v ->
> 		let rec loopu acc sol board = function
> 		  | -1 -> loopv acc sol board (v - 1)
> 		  | u ->
> 		    let c = get u v
> 		    in
> 		    if c = ' '
> 		    then loopu acc sol board (u - 1)
> 		    else if B.get board (x + u) (y + v) = ' '
> 		    then
> 		      begin
> 			let board = B.set board (x + u) (y + v) c
> 			in
> 			loopu acc ((c, x + u, y + v)::sol) board (u - 1)
> 		      end
> 		    else loopx acc (x - 1)
> 		in
> 		loopu acc sol board (width - 1)
> 	    in
> 	    loopv acc [] B.board (height - 1)
> 	in
> 	loopx acc (B.width - width)
>    in
>    loopy [] (B.height - height)
>
>  let print (sol, board) =
>    B.print board;
>    Array.iter
>      (fun (c, x, y) ->
> 	Printf.printf "%c: (%c, %d)\n" c
> 	  (char_of_int (int_of_char 'A' + x))
> 	  (y + 1))
>      sol;
>    flush_all ()
> end
>
> module D = struct
>  let infty = 999999
>  let make_one x y =
>    let d = Array.make_matrix B.width B.height infty in
>    let rec loop n acc = function
>      | [] ->
> 	if acc = []
> 	then d
> 	else loop (n + 1) [] acc
>      | (u, v)::xs ->
> 	let rec move acc x y dx dy =
> 	  if B.get B.board x y = ' '
> 	  then
> 	    let acc =
> 	      if d.(x).(y) > n
> 	      then
> 		begin
> 		  d.(x).(y) <- n;
> 		  (x, y)::acc
> 		end
> 	      else acc
> 	    in
> 	    move acc (x + dx) (y + dy) dx dy
> 	  else acc
> 	in
> 	let acc = move acc u v (-1) 0 in
> 	let acc = move acc u v 1 0 in
> 	let acc = move acc u v 0 (-1) in
> 	let acc = move acc u v 0 1
> 	in
> 	loop n acc xs
>    in
>    d.(x).(y) <- 0;
>    loop 1 [] [(x, y)]
>
>  let dist =
>    Array.init B.width (fun x -> Array.init B.height (fun y ->  
> make_one x y))
>
>  let get x1 y1 x2 y2 =
>    if (x1 < 0) || (x1 >= B.width) || (y2 < 0) || (y2 >= B.height)
>      || (x2 < 0) || (x2 >= B.width) || (y2 < 0) || (y2 >= B.height)
>    then infty
>    else dist.(x1).(y1).(x2).(y2)
>
>  let get_all pos =
>    let d =
>      Array.mapi
> 	(fun i (c, x1, y1) ->
> 	  let (_, x2, y2) = B.start.(i)
> 	  in
> 	  get x1 y1 x2 y2)
> 	pos
>    in
>    Array.fold_left ( + ) 0 d
> end
>
> module S = struct
>  type dir = NORTH | SOUTH | WEST | EAST
>
>  let max_moves = 1000
>  let cache = Hashtbl.create 0
>    (*
>  let states = ((Array.make max_moves []) :
>      ((int * int * dir) list * (char * int * int) array * string)  
> list array)
>    *)
>  let states = Array.make max_moves []
>
>  let string_of_dir = function
>    | NORTH -> "norden"
>    | SOUTH -> "sueden"
>    | WEST -> "westen"
>    | EAST -> "osten"
>
>  let print (moves, (_ : (char * int * int) array), board) =
>    B.print board;
>    List.iter
>      (fun (x, y, dir) ->
> 	Printf.printf "zug %c %d %s,"
> 	  (char_of_int (int_of_char 'A' + x))
> 	  (y + 1)
> 	  (string_of_dir dir))
>      moves
>
>  let num_states =
>    List.fold_left
>      (fun num (sol, board) ->
> 	let d = D.get_all sol in
> 	let state = ([], sol, board)
> 	in
> 	Hashtbl.add cache board ();
> 	states.(d) <- state::states.(d);
> 	print state;
> 	num + 1)
>      0
>      G.solutions
> end
>
> let () =
>  List.iter G.print G.solutions;
>  Printf.printf "%d solutions\n" (List.length G.solutions)
>
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Odd failure to infer types

[Guillaume Yziquel]

Le Saturday 03 Sep 2011 à 11:53:30 (+0200), Goswin von Brederlow a écrit :
> Hi,
> 
> I'm implementing a solver for the game Atomix. If you don't know it then
> don't worry. It isn't relevant.
> 
> I split things up into submodules and now one of the submodules does not
> infere the right types:
> 
> File "Atomix.ml", line 168, characters 11-876:
> Error: The type of this module,
>        sig
>          type dir = NORTH | SOUTH | WEST | EAST
>          val max_moves : int
>          val cache : (string, unit) Hashtbl.t
>          val states :
>            ('_a list * (char * int * int) array * string) list array
>          val string_of_dir : dir -> string
>          val print :
>            (int * int * dir) list * (char * int * int) array * string -> unit
>          val num_states : int
>        end, contains type variables that cannot be generalized
> 
> I believe this is wrong. In S.num_states the call to "print state"
> fixates the type for state and the "states.(d) <- state::states.(d);"
> should then fixate the missing '_a in the type for states.
> 
> Anyone know why?

It also seems quite wrong to me. You should perhaps file a bug into
Mantis if no typing expert answers.

Did you try adding type annotations one at a time near the call to print
and the states.(d) assignment in your anonymous List.fold-ing function?
To check precisely what the type inferencer gets right and what it gets
wrong?

I'd be curious to know whether annotating state in "states.(d) <-
state::states.(d)" solves your problem. Since it's here that the '_a in
the type of states should be fixated.

-- 
     Guillaume Yziquel

Re: [Caml-list] Odd failure to infer types

[Philippe Veber]

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

Hi, I'm really no typing expert and have not looked much into your code, so
sorry in advance if what I say is irrelevant. Christophe got it right I
think : I'd say that an array value cannot be polymorphic because it is
mutable. I've quickly searched the web and found that

http://mirror.ocamlcore.org/caml.inria.fr/pub/ml-archives/caml-list/2001/12/0dccd30f4582e551a674562e3ddcc03c.en.html

Quoting François Pottier:
"Any polymorphic, mutable structure is unsound and rightly rejected. A
monomorphic, mutable structure that contains polymorphic data is sound, but
cannot be expressed in ML's type system where universal quantification must
be prenex."

So it seems to me that whatever the way you try to achieve it, you simply
can't define a value state of type

val states : ('a list * (char * int * int) array * string) list array

(implicitely for all 'a). If the compiler is right, you'll always end up
with a weak type variable somewhere.

my 2 cent,

ph.


2011/9/3 Guillaume Yziquel <guillaume.yziquel@citycable.ch>

> Le Saturday 03 Sep 2011 à 11:53:30 (+0200), Goswin von Brederlow a écrit :
> > Hi,
> >
> > I'm implementing a solver for the game Atomix. If you don't know it then
> > don't worry. It isn't relevant.
> >
> > I split things up into submodules and now one of the submodules does not
> > infere the right types:
> >
> > File "Atomix.ml", line 168, characters 11-876:
> > Error: The type of this module,
> >        sig
> >          type dir = NORTH | SOUTH | WEST | EAST
> >          val max_moves : int
> >          val cache : (string, unit) Hashtbl.t
> >          val states :
> >            ('_a list * (char * int * int) array * string) list array
> >          val string_of_dir : dir -> string
> >          val print :
> >            (int * int * dir) list * (char * int * int) array * string ->
> unit
> >          val num_states : int
> >        end, contains type variables that cannot be generalized
> >
> > I believe this is wrong. In S.num_states the call to "print state"
> > fixates the type for state and the "states.(d) <- state::states.(d);"
> > should then fixate the missing '_a in the type for states.
> >
> > Anyone know why?
>
> It also seems quite wrong to me. You should perhaps file a bug into
> Mantis if no typing expert answers.
>
> Did you try adding type annotations one at a time near the call to print
> and the states.(d) assignment in your anonymous List.fold-ing function?
> To check precisely what the type inferencer gets right and what it gets
> wrong?
>
> I'd be curious to know whether annotating state in "states.(d) <-
> state::states.(d)" solves your problem. Since it's here that the '_a in
> the type of states should be fixated.
>
> --
>      Guillaume Yziquel
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

Re: [Caml-list] Odd failure to infer types

[Guillaume Yziquel]

Le Saturday 03 Sep 2011 à 12:31:59 (+0200), Christophe Papazian a écrit :
> The type of [] is 'a list. This is (strong) polymorphism. Calling a
> function 'int list -> ?' on [] doesn't not
> remove the polymorphism of []. However, an '_a list array is not
> polymorphism, it's just the compiler who don't know
> yet the type inside the lists. And as you give him [], he can't
> deduce the type.
> 
> As an example you can do this :
> 
> let s = [] in 1::s, 'a'::s, [|s|]	;;
> 
> And it still doesn't know...

Ah, right... not the most obvious case though for let-polymorphism.

A perhaps more talking example would be

	let f x = x in (f 1, f "1")

While let-polymorphism makes obvious sense when using f as a function,
it's less intuitive when it used on a function argument such as [],
though quite logical.

Personnally, I find it quite weird to have the value restriction on list
refs, but not on lists:

	# let x = [];;
	val x : 'a list = []

	# let x = ref [];;
	val x : '_a list ref = {contents = []}

	# let x = [] in (List.map print_string x), (List.map print_int x);;
	- : unit list * unit list = ([], [])

	# let x = ref [] in (List.map print_string !x), (List.map print_int !x);;
	Error: This expression has type string list
	       but an expression was expected of type int list

Using the print function on a state which doesn't have [] as first
component of the tuple would likely fixate properly the '_a, though.

-- 
     Guillaume Yziquel

Re: [Caml-list] Odd failure to infer types

[Guillaume Yziquel]

Le Saturday 03 Sep 2011 à 13:35:22 (+0200), Philippe Veber a écrit :
>    Hi, I'm really no typing expert and have not looked much into your
>    code, so sorry in advance if what I say is irrelevant. Christophe got
>    it right I think : I'd say that an array value cannot be polymorphic
>    because it is mutable. I've quickly searched the web and found that
>    [1]http://mirror.ocamlcore.org/caml.inria.fr/pub/ml-archives/caml-list/
>    2001/12/0dccd30f4582e551a674562e3ddcc03c.en.html

Yes, Christophe got it right.

While not having the let-restriction on [] seems right theoretically, I
see little practical use case for it however.

-- 
     Guillaume Yziquel

Re: [Caml-list] Odd failure to infer types

[Gabriel Scherer]

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

Indeed, a let-bound [] is generalized to a polymorphic ('a list), while a
let-bound (ref []), or (Array.make n []), is not generalized. It would be
unsound to do so as if you had a reference to a polymorphic ('a list) you
could add elements of different types in the list.

When a type variable is not generalized (polymorphic), it stays an "unknown"
of the type system until it is unified to a known type:

# let r = ref [];;
val r : '_a list ref = {contents = []}
# r := 1 :: !r;;
- : unit = ()
# r;;
- : int list ref = {contents = [1]}

'_a is sometimes called a "weakly polymorphic variable", in fact it is not
polymorphic at all. It is just an unknown.

In the code example above, the real type for '_a could be determined after
two phrases in the top level. It may also happen as a compilation unit (if
the code was written in a file instead of fed phrase-per-phrase to the
toplevel). We wouldn't observe the intermediary '_a inferred type, as the
type are inferred globally.

It is forbidden however to keep an "undetermined variable" in a module
interface. This is what the error message here says: the variable '_a could
neither be generalized (as it is not a let-bound value, but a reference
resulting from a call to the "ref" function), nor determined by unification
with something in the module.
Keeping undetermined variables in a module interface would break the
separate compilation permitted by the interface/implementation distinction
at the module level. Indeed, if a module A had undetermined variables in its
interface, and modules B and C used A, B and C would have to coordinate each
other to make sure that the instantiations they make (for the undetermined)
are compatible; you couldn't compile B with A, and C with A, separately.

The solution is to give enough indications locally, in the module, so that
the reference type can be determined:

 let states = Array.make ... ([] : (int * int * dir) list * (char * int *
int) array * string)




It also seems quite wrong to me. You should perhaps file a bug into
> Mantis if no typing expert answers.
>

I don't want to criticize your answer which was very helpful, but I would
like to point out that I have seen the "when you don't understand the type
checker, it may be a bug" reaction quite often on this list. Indeed, all
software has failures and the OCaml type checker is not exempt of bugs, most
particularly on the delicate or recently changed parts of the system (first
class modules, etc.).

In general, the type checker is quite solid. I personally find that thinking
of a tool bug when I'm stuck on something is actually counter-productive in
most situations; when debugging something, you need strong guarantees of
what "is right" and what "may have gone wrong". Insinuating doubts against
the tool (on which you have no control) is a good way, at least for me, to
not push myself into really thinking about what I could have done wrong on
my side. Therefore, I try to always assume that the tools are right (and in
my case working with the OCaml typechecker, they have never failed me),
because it saves me lots of doubts, confusion, and self-indulgence.


On Sat, Sep 3, 2011 at 1:46 PM, Guillaume Yziquel <
guillaume.yziquel@citycable.ch> wrote:
> Le Saturday 03 Sep 2011 à 13:35:22 (+0200), Philippe Veber a écrit :
>>    Hi, I'm really no typing expert and have not looked much into your
>>    code, so sorry in advance if what I say is irrelevant. Christophe got
>>    it right I think : I'd say that an array value cannot be polymorphic
>>    because it is mutable. I've quickly searched the web and found that
>>    [1]
http://mirror.ocamlcore.org/caml.inria.fr/pub/ml-archives/caml-list/
>>    2001/12/0dccd30f4582e551a674562e3ddcc03c.en.html
>
> Yes, Christophe got it right.
>
> While not having the let-restriction on [] seems right theoretically, I
> see little practical use case for it however.
>
> --
>     Guillaume Yziquel
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

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

Re: [Caml-list] Odd failure to infer types

[Guillaume Yziquel]

Le Saturday 03 Sep 2011 à 14:15:35 (+0200), Gabriel Scherer a écrit :
>
>    [...]

Thanks for your explanation, which is quite thorough.

>      It also seems quite wrong to me. You should perhaps file a bug into
>      Mantis if no typing expert answers.
> 
>    I don't want to criticize your answer which was very helpful, but I
>    would like to point out that I have seen the "when you don't understand
>    the type checker, it may be a bug" reaction quite often on this list.

Well, there was an "if" clause... Nevertheless I agree that the
type checker is quite solid. I only had "serious" problems (infinite
loops) when playing too harshly with subtyping or recursive types.

-- 
     Guillaume Yziquel

Re: [Caml-list] Odd failure to infer types

[Goswin von Brederlow]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> Indeed, a let-bound [] is generalized to a polymorphic ('a list), while a
> let-bound (ref []), or (Array.make n []), is not generalized. It would be
> unsound to do so as if you had a reference to a polymorphic ('a list) you could
> add elements of different types in the list.
>
> When a type variable is not generalized (polymorphic), it stays an "unknown" of
> the type system until it is unified to a known type:
>
> # let r = ref [];;
> val r : '_a list ref = {contents = []}
> # r := 1 :: !r;;
> - : unit = ()
> # r;;
> - : int list ref = {contents = [1]}
>
> '_a is sometimes called a "weakly polymorphic variable", in fact it is not
> polymorphic at all. It is just an unknown.
>
> In the code example above, the real type for '_a could be determined after two
> phrases in the top level. It may also happen as a compilation unit (if the code
> was written in a file instead of fed phrase-per-phrase to the toplevel). We
> wouldn't observe the intermediary '_a inferred type, as the type are inferred
> globally.

I think you are missing the point.

I totaly get why it must be '_a instead if 'a. My question is why it
doesn't infer the full type from the call to the print function.

In my case the type inferences outputs something like this (using the
above example):

> # let r = ref [];;
> val r : '_a list ref = {contents = []}
> # r := 1 :: !r;;
> - : unit = ()
> # r;;
> - : '_a list ref = {contents = [1]}

I see my print call as equivalent to '1 :: !r'.

MfG
        Goswin

Re: [Caml-list] Odd failure to infer types

[Gabriel Scherer]

On Sat, Sep 17, 2011 at 2:08 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> I think you are missing the point.
>
> I totaly get why it must be '_a instead if 'a. My question is why it
> doesn't infer the full type from the call to the print function.

You're correct, I was missing your point. You have the following situation:

 let num_states =
  List.fold_left
    (fun num (sol, board) ->
      let d = D.get_all sol in
      let state = ([], sol, board)
      in
      Hashtbl.add cache board ();
      states.(d) <- state::states.(d);
      print state;
      num + 1)
    0
    G.solutions

with the following inferred types:
 states: ('_a list * (char * int * int) array * string) list array
 print: (int * int * dir) list * (char * int * int) array * string -> unit

(Remark: the types given above are the result of calling
"caml-types-show-type" in an Emacs buffer, after compiling the fail
with -annot; we get partial type information even when the compilation
fail)

Why doesn't the type of "states" get inferred from the call to `print state`?
The reason why is that `state`, contrarily to `states`, is
polymorphic. It has type (caml-types...) 'b list * (char * int * int)
array * string, because the empty list [] has polymorphic type.
Therefore, it can be used in two different contexts with *different*
types (instantiations) that don't get unified with each other
 states.(d) <- state::states.(d);
 print state;
on the first line, the type 'b list of [] is instantiated to a fresh
type then unified with the '_a list of states, and on the second line
it is instantiated again, independently, and the resulting fresh type
is unified with (int * int * dir) list.

You can see that this is the problem by forcing the list to have a
monomorphic type:
 let mono_list = ref [] in
 let state = (!mono_list, sol, board)
With this (indeed unreadable) version, your whole code compiles fine.
Another technique to do that would be:
 print (List.hd states.(d));

(I would still rather use a type annotation on the 'states' variable)