John Fremlin's blog: Subverting the OCaml type system

Waiting for updates: connected

I had a program that generated a report of a few interesting numerical results from an experiment (number of packets lost, number of packets received, mean latency, etc.). These statistics might have a high variance or might be very tightly distributed. To investigate, I ran multiple experiments with the same parameters. Now I wanted to generate a summary table with some statistics on the per experiment statistics (maximum packets lost across all runs, etc.).

One small polish on the obvious design is that the summary program should calculate and output the latency statistics in floating point format but the maximum of the packets lost is clearly an integer, and should be output as such.

In OCaml, we can define a union datatype that allows for both types of values or an undefined value.

type num = I of int | F of float | N;;

How about taking the maximum of a pair of nums? The max function (and at a lower level the > function) can be applied to a pair of ints or a pair of floats. You might think that this would work

let lift2broken f x y =
  match (x,y) with
    | (I i) ,(I j) -> I (f i  j)
    | (F i), (F j) -> F (f i  j);;

Then to convert the max function to something that would work on nums, you would do (lift2broken max). But lift2broken does not compile: Error: This expression has type float but an expression was expected of type int.

The problem is that the type of max (and of f) is 'a -> 'a -> 'a, but on encountering the first use of f, i.e. I (f i j), the unspecified type 'a is unified with int.

Adrien Pierard helped me to this solution

let lift2if f_I f_F  x y =
  match (x,y) with
    | (I i) ,(I j) -> I (f_I i  j)
    | (F i), (F j) -> F (f_F i  j);;
 
let lift2 f =
  let fi = f
  and ff = Obj.magic f
  in lift2if fi ff;;

In some ways, it seems very unfortunate that something as simple as this requires one to break out of the type system with Obj.magic, and shows a crack in the illusion that functions with variable types are really functions . . . I'm very new to the language and I wonder if there isn't a better way to do it? Presumably there are ML dialects where this issue is finessed?

Here is the complete program.