Type inference inside exceptions ?

[Diego Olivier FERNANDEZ PONS <diego.fernandez_pons@etu.upmc.fr>]

     Bonjour,

I would like the type-checker to infer the type inside exceptions (or  
at least to help me in the "guess a type and test" loop).

More specifically, here is my problem:

I have a program that computes the optimal solution of the minimal  
cardinality subset-sum problem with multiplicities. In simple words it  
gives the minimum number of coins you need to reach a given amount of  
money.

val smc : int -> int list -> int list list * int = <fun>
# smc 226 [198; 122; 90; 75; 64; 54; 53; 10; 5; 1];;
- : int list list * int =
([[75; 75; 75; 1]; [122; 64; 10; 10; 10; 10]; [198; 10; 10; 5; 1; 1; 1]],
  198105)

The programs gives all the solutions it found, the last one being the  
optimal (with the total number of backtracks). The best solution is  
kept by side-effects on a global variable.

type environment = {
     mutable solutions : int list list;
     mutable backtracks : int;
     mutable card : int
   }

exception Fail

let rec min_card env = fun to_reach chosen candidates ->
   if (to_reach = 0) then
     match compare env.card (List.length chosen) with
       | n when n <= 0 ->
	  env.backtracks <- env.backtracks + 1;
	  raise Fail
       | _ ->
	  env.solutions <- chosen :: env.solutions;
	  env.card <- List.length chosen;
	  raise Fail
   else
     match candidates with
       | [] ->
	  env.backtracks <- env.backtracks + 1;
	  raise Fail
       | x :: tail when x > to_reach -> min_card env to_reach chosen tail
       | x :: tail ->
	  try
	    min_card env (to_reach - x) (x :: chosen) candidates
	  with Fail ->
	    min_card env to_reach chosen tail

let rec smc = fun to_reach list ->
   let env = { solutions = []; backtracks = 0; card = max_int } in
     try
       min_card env to_reach [] (List.sort (fun x y -> compare y x) list)
   with Fail -> (List.map List.rev env.solutions, env.backtracks)

Now I want the program not to return all the solutions but only the  
first solution it found and a list of continuations that I can launch  
again if a better solution is required.

Therefore I add a second exception
type continuation = ...
exception Solution of int * continuation list

And I collect the continuations from the try ... catch when the left  
tree happens to contain a solution

try
    explore left subtree
with
   | Fail -> explore right subtree
   | Solution (s, cont) ->
     let c = function () -> explore right subtree in
       raise Solution (s, c :: cont)

Not knowing the type of the continuation, I just tried unit -> int

Here is the detailed code

type continuation = unit -> int
exception Solution of int * continuation list

let rec min_card env = fun to_reach chosen candidates ->
   if (to_reach = 0) then
     match compare env.card (List.length chosen) with
       | n when n <= 0 ->
	  env.backtracks <- env.backtracks + 1;
	  raise Fail
       | _ ->
	  env.solutions <- chosen :: env.solutions;
	  env.card <- List.length chosen;
	  raise (Solution (List.length chosen, []))
   else
     match candidates with
       | [] ->
	  env.backtracks <- env.backtracks + 1;
	  raise Fail
       | x :: tail when x > to_reach -> min_card env to_reach chosen tail
       | x :: tail ->
	  try
	    min_card env (to_reach - x) (x :: chosen) candidates
	  with
	    | Fail -> min_card env to_reach chosen tail
	    | Solution (s, continuation) ->
		let c = fun () -> min_card env to_reach chosen tail in
		  raise (Solution (s, (c :: continuation)))

I first wrap without catching the exceptions and test

let smc = fun to_reach list ->
   let env = { solutions = []; backtracks = 0; card = max_int } in
       min_card env to_reach [] list

# val smc : int -> int list -> int = <fun>
# smc 226 [198; 122; 90; 75; 64; 54; 53; 10; 5; 1];;
Exception: Solution (7, [<fun>; <fun>; <fun>; <fun>; <fun>; <fun>; <fun>]

Seems correct.

Now I try to extract the integer

let smc = fun to_reach list ->
   try
     let env = { solutions = []; backtracks = 0; card = max_int } in
       min_card env to_reach [] list
   with Solution (c, l) -> c

# val smc : int -> int list -> int = <fun>
# smc 226 [198; 122; 90; 75; 64; 54; 53; 10; 5; 1];;
- : int = 7

Correct.

Now I try to extract the continuation list

let smc = fun to_reach list ->
   let env = { solutions = []; backtracks = 0; card = max_int } in
     try
       min_card env to_reach [] list
     with Solution (c, l) -> l

This expression has type continuation list but is here used with type int

Ok. I have to correct the type of continuation by hand

lets try [type continuation = unit -> (unit -> int)]

This expression has type continuation list but is here used with type
   unit -> int

lets try [type continuation = Cont of (unit -> continuation)]
and [let c = Cont (fun () -> ... ) in raise Solution (s, c :: cont)]

This expression has type continuation list but is here used with type
   continuation

lets try [type continuation = Cont of (unit -> continuation list)]

# val smc : int -> int list -> continuation list = <fun>
# smc 226 [198; 122; 90; 75; 64; 54; 53; 10; 5; 1];;
- : continuation list =
[Cont <fun>; Cont <fun>; Cont <fun>; Cont <fun>; Cont <fun>; Cont <fun>;
  Cont <fun>]

Great ! Now I want the solution, its cardinality and the continuation list

lets try ...

          Diego Olivier