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

The correct way to port this exact piece of code (which I think comes from this webpage ) is to use first-class polymorphism, as described in this FAQ article: How do I write a function with polymorphic arguments? Please read the FAQ section, but here's one example of working code for quick reference:

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 need this first-class polymorphism here. As far as parameterization is concerned, the only thing that printer

can do with the data of the type 'a

is to pass it to the print function 'a → string

. Thus, the behavior of the printer is completely determined by what it does with the resulting string

data. In other words, a 'b printer

type 'b printer

is isomorphic to a string → 'b

type string → 'b

; it carries no other information. Thus, 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!")

      

        
        
        
      

    

Type foo

now (string → 'a) → t → 'a

. This is called continuation passing style: the only way to deduce 'a

from this type is to call the argument function on the string, so you don't really do anything other than return the string and call the function (continuation) on that. It 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 showed is overly complex and the problem it seems to pose is overblown. There is no need for a complex type system. (But you can certainly find better examples where first-class polymorphism, as demonstrated in the FAQ, is really useful. It happens that this example ... sucks.)

Historical and scientific context

Historical digression about first-class polymorphism as requested by the question.

'a. ('a → string) → 'a → 'b

'a. ('a → string) → 'a → 'b

means "for everyone 'a

, ('a → string) → 'a → 'b

". It is a type that is polymorphic in a type variable 'a

(which is "defined" with 'a.

Bit) and has a free variable 'b

(which is defined as a type parameter printer

).

The type foo

in the first version of the code above is 'b printer → t → 'b

. This can be understood as System F type encoding

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

      

        
        
        
      

    

The ML type inference algorithm is a type limited by "prefix polymorphism", that is, types whose all type variables are quantified at the beginning. This is the case 'b

in the above type, but not 'a

which is quantified within the (polymorphic) argument. Type systems that adhere exactly to this ML (Hindley-Damas-Milner) inference constraint will not infer that type, and therefore reject programs that need it as incorrectly typed (which means not "wrong" but "i can't prove it right ").

This constraint makes the inference system both decidable (type inference for the complete System F is undecidable (Joe B. Wells)) and "principled" (see this SO discussion if you don't know what basic types are; in short, it is means that the inference engine always chooses the most general type), but it also rejects well-typed programs, which is a common blow to type-safe systems.

Most ML languages ​​(OCaml, Haskell ...) ran into this limitation at some point for code they really wanted to be able to write. For OCaml coming in the nineties while working on coding 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 then extended to records (first-class modules are an independent and much newer addition that also allows this). There is a good reason why this is still more or less limited to "things" that have "fields" in a way, because it gives a natural way of placing (required) polymorphism annotations, and field projection is a good place for a type checker to check need to create a polymorphic value - this simplifies theory if you like.

For research work during this period in the OCaml community, see, for example, ML Extension with Higher Order Semi-Explicit Polymorphism , Jacques Garrigue and Didier Rémy, 1997. A different approach to first class polymorphism was developed (see Section 5 (Related Works) by Dider Le Botlan Recasting MLF for Literature Review), and other use cases were found, notably the ST

Haskell monad ( Lazy Functional State Threads , Simon Peyton Jones and John Launchbury, 1994).