Re: [Caml-list] Why type inference fails in this code

[Jeremy Yallop <yallop@gmail.com>]

Dear Rouan,

2009/10/9  <rouanvd@softwarerealisations.com>:
> type t = MyInt of int | MyFloat of float | MyString of string ;;
>
> let foo printerf = function
>  | MyInt i -> printerf string_of_int i
>  | MyFloat x -> printerf string_of_float x
>  | MyString s -> printerf (fun x -> x) s

This fails because the variable "printerf" is used at different types
inside the body of foo.  OCaml's type system requires function
arguments to be used at the same type everywhere they appear in the
body of the function.  The reason is simple: without this restriction
type inference becomes undecidable.

The most reasonable type for foo seems like the following:

   forall 'b. (forall 'a. ('a -> string) -> 'a -> 'b) -> t -> 'b

which is the type of a function that constructs a value of type 'b
from a value of type t using its argument function; this argument
function takes a printer for any type 'a and a value of type 'a and
constructs a value of type 'b.

We can make two adjustments to "foo" to turn it into something that
OCaml will accept.  The first adjustment is to turn the argument
"printerf" into an object with a single method; polymorphic types
(i.e. types that use "forall") in OCaml must be wrapped in object or
record types.  The second adjustment is to provide a type signature,
which changes the impossible problem of type /inference/ into the
easier problem of type /checking/.  Here is the revised definition:

  let foo : < p : 'a . ('a -> string) -> 'a -> 'b > -> t -> 'b =
    fun printerf -> function
      | MyInt i    -> printerf#p string_of_int i
      | MyFloat x  -> printerf#p string_of_float x
      | MyString s -> printerf#p (fun x -> x) s

In order to call this function we must, of course, ensure that the
first argument is an object.  Here is a simple example, where the
argument just returns the constructed string:

   foo (object method p : 'a. ('a -> string) -> 'a -> string = fun x
-> x end) (MyInt 3)

Hope this helps,

Jeremy.