Polymorphic variants and variance

Question

I am attempting to create a procedural object language system in OCaml. The general idea is to store values of polymoprhic variants in an array and let procedures update this array (imperatively):

module StrMap = Map.Make(String) 

module IntMap = Map.Make(struct type t = int let compare = compare end)

(* store generic labeled objects *)
type 'a env = ([> ] as 'a) IntMap.t

(* a procedure working on such an object array *)
type 'a procedure = 'a env -> 'a env

(* store procedures *)
type 'a proc_table = ('a procedure) StrMap.t

let do_iinc = function 
  | `Int n -> `Int (n+1)

let iinc x env = 
  let v = do_iinc (IntMap.find x env) in 
  IntMap.add x v env

let do_finc = function 
  | `Float f -> `Float (f +. 1.0)

let finc x env = IntMap.add x (do_finc (IntMap.find x env)) env

(* type error :( *)
let table  = 
  StrMap.add "iinc" (iinc 0)
         (StrMap.add "finc" (finc 1)
                 StrMap.empty)

This puzzles me. My "update" is invariant for a concrete type. Shouldn't OCaml be able to figure out that table : ([`Float of float ; `Int of int ] procedure) StrMap.t ?

I suspect the problem has to do with the variance of map, but I fail to confirm it, since I cannot annotate the type with the concrete polymorphic variants.

Is my idea even feasible in OCaml?

Answer 1

The type of this function:

let do_finc = function 
  | `Float f -> `Float (f +. 1.0)

Is [< `Float of float ] -> [> `Float of float ]. In other words, it takes as input any variant type that has at most a `Float alternative; i.e., either has a `Float alternative, or no alternatives at all. It seems to me you want the function to work for variants that have at least a `Float alternative , i.e., a variant that has `Float and any number of other variants:

let do_finc = function 
  | `Float f -> `Float (f +. 1.0)
  | _ -> failwith "wanted a float"

If I change do_iinc and do_finc in this way, the table has a type closer to what you want.

I'm not at all sure that your plan will work, as you might be expecting OCaml to accept type-incorrect programs and complain at runtime. Instead OCaml complains at compile time and you probably have to write your own code to complain at runtime :-) But this might help get past the first problem.

Answer 2

I'm not entirely clear on what you are trying to do, but it looks unsafe to me.

Your finc 1 does not have type [`Float of float ; `Int of int ] procedure as you suggest, it has type [`Float of float ] procedure which is equivalent to [`Float of float] IntMap.t -> [`Float of float] IntMap.t.

This is because the do_finc function, which you apply to a member of your argument env, only knows how to handle [`Float of float] -- it has no case for [`Int of int].

If table had the type you wanted consider what would happen in the following expression:

let f = StrMap.find "finc" table in
let m = IntMap.add 1 (`Int 4) IntMap.empty in
  f m