What's the correct way to write this in OCaml?

Question

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

It reports:

Error: This expression has type float -> string
       but an expression was expected of type int -> string

Answer 1

The right way to port this exact code snippet (which, I guess, is coming from this webpage) is to use first-class polymorphism as explained in this FAQ entry: How to write a function with polymorphic arguments?. Please go read the FAQ entry, but for quick reference here is one example of working code:

type t = MyInt of int | MyFloat of float | MyString of string

type 'b printer = { print : 'a . ('a -> string) -> 'a -> 'b }
let foo erf = function
  | MyInt i -> erf.print string_of_int i
  | MyFloat x -> erf.print string_of_float x
  | MyString s -> erf.print (fun x -> x) s

let () = foo
  { print = fun printer data -> print_endline (printer data) }
  (MyString "Hello World!")

Note, however, that you don't actually need this first-class polymorphism here. By parametricity, the only thing the printer can do with the data of type 'a is to pass it to the printing function 'a -> string. So the behavior of the printer is entirely determined by what it does to the resulting string data. Said another way, the type 'b printer is isomorphic to the type string -> 'b, it brings no other information. So you can write:

let foo erf = function
  | MyInt i -> erf (string_of_int i)
  | MyFloat x -> erf (string_of_float x)
  | MyString s -> erf s

let () = foo print_endline (MyString "Hello World!")

The type of foo is now (string -> 'a) -> t -> 'a. This is known as continuation-passing style: the only way to get an 'a out of this type is to call the argument function on a string, so in fact you're doing nothing more than returning a string, and calling the function (continuation) on it. This can be rewritten as:

let foo = function
  | MyInt i -> string_of_int i
  | MyFloat x -> string_of_float x
  | MyString s -> s

let () = print_endline (foo (MyString "Hello World!"))

Long story short: the code you've shown is overly complicated, and the problem it appears to pose is overblown. There is no need for a complex type system here. (But you certainly can find better examples where first-class polymorphism as demonstrated in the FAQ is actually useful. It only happens that this example... sucks.)

Historical and scientific context

An historic aside on first-class polymorphism, requested by the question.

'a . ('a -> string) -> 'a -> 'b means "for all 'a, ('a -> string) -> 'a -> 'b". It is a type that is polymorphic in the type variable 'a (which is "defined" by the 'a . bit), and has a free variable 'b (which is defined as a parameter of the printer type).

The type of foo in the first version of the code above is 'b printer -> t -> 'b. It can be understood as encoding the System F type

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

The ML type inference algorithm is infers type restricted to "prefix polymorphism", that is types whose all type variables are quantified at the front. This is the case of 'b in the type above, but not of 'a that is quantified inside a (polymorphic) argument. Type systems that exactly respect this restriction of the ML (Hindley-Damas-Milner) inference system will not infer this type, and therefore reject programs that need it as ill-typed (meaning not "wrong" but "I cannot prove it's right").

This restriction makes the inference system both decidable (type inference for full System F is undecidable (Joe B. Wells)) and "principal" (see this SO discussion if you don't know what principal types are; in short, it means that the inference engine always pick the most general type), but it also rejects well-typed programs, the usual bane of safe type systems.

Most ML languages (OCaml, Haskell...) have at some point encountered this limitation for code that they really wanted to be able to write. For OCaml that came in the nineties, when working on encoding object-oriented programming patterns in the language (see examples in the manual).

This is why first-class polymorphism was first introduced in method types, and later extended to records (first-class modules are a independent and much more recent addition that also allows this). There is a good reason why this is still more or less restricted to "things" that have "fields" in some sense, because this gives a natural way to place the (necessary) polymorphism annotations, and field projection is a good place for the type-checker to test the need to instantiate a polymorphic value -- this makes the theory simpler, if you will.

For research work in this period in the OCaml community, see for example Extending ML with Semi-Explicit Higher-Order Polymorphism, Jacques Garrigue and Didier Rémy, 1997. Other approach to first-class polymorphism have been developed (See section 5 (Related Works) of Dider Le Botlan's Recasting MLF for an overview of the literature), and other use cases have been found, notably the ST monad in Haskell (Lazy Functional State Threads, Simon Peyton Jones and John Launchbury, 1994).

Answer 2

From this line

| MyInt i -> printerf string_of_int i

compiler infers that 1st argument of printerf should have type int -> string, but from the next line

| MyFloat x -> printerf string_of_float x

It seems that 1st argument of printerf should be a float -> string. I think that you know that OCaml has different types for integer and real numbers... So this collision in type of printerf makes compiler sick.

What type did you expect as type of printerf in this code? Maybe you should avoid high-order functions and implement convertion to string more straightforward?