Map a subset of a polymorphic variant

Question

I often want to apply a function to the values inside some variant, so that the result of the function has the same type as the input. How can I make the types work out? Here's my current attempt:

module T : sig
  type generic =
    [ `Foo of int
    | `Bar of int ]

  val map : (int -> int) -> ([< generic] as 'a) -> 'a

(*   val a : [`Foo of int] *)
end = struct
  type generic =
    [ `Foo of int
    | `Bar of int ]

  let map fn = function
    | `Foo x -> `Foo (fn x)
    | `Bar x -> `Bar (fn x)
  let map : (int -> int) -> ([< generic] as 'a) -> 'a = Obj.magic map

(*
  let a : [`Foo of int] = `Foo 1 |> map succ
  let b : [`Bar of int] = `Bar 1 |> map succ
*)
end

This works as-is, but if I uncomment the let a line then I get:

   Values do not match:
     val map : (int -> int) -> [ `Foo of int ] -> [ `Foo of int ]
   is not included in
     val map : (int -> int) -> ([< generic ] as 'a) -> 'a

It seems like defining a has changed the type of map, which seems odd.

On the other hand, putting this after the end of the module works:

open T
let a : [`Foo of int] = `Foo 1 |> map succ
let b : [`Bar of int] = `Bar 1 |> map succ

Finally, if I change the definition of map to:

  let map : 'a. (int -> int) -> ([< generic] as 'a) -> 'a = Obj.magic map

(i.e. just adding an explicit 'a. to the start) then it complains:

Error: This definition has type (int -> int) -> ([< generic ] as 'a) -> 'a
   which is less general than
     'b. (int -> int) -> ([< generic ] as 'b) -> 'b

Can someone explain what's going on? Is there a better way to do this? I can use a GADT to avoid the Obj.magic, but then I have to pass it to every function call, which I'd like to avoid.

Note about the real system

In my actual program, I have various node types (Area, Project, Action, Contact, etc) and different operations apply to different types, but some are common.

For example, with_name can rename any node type, but if I rename an Action then the result must be another action. If I rename an [Area | Project | Action] then the result must be an [Area | Project | Action], etc.

I originally used a tuple, with the common details outside (e.g. (name * Action ...)) but this makes it hard for users to match on the different types (especially as they're abstract) and some features are common to subsets (e.g. only Projects and Actions can be starred).

Answer 1

You just got bite by the value restriction. The typechecker, not knowing the types in Obj.magic map and in particular, their injectivity/variance, can't immediately generalize and waits for a module boundary. If you look with merlin, it shows you this type : (int -> int) -> (_[< generic ] as 'a) -> 'a. Notice the _ which shows a monomorphic type variable. The type variable get specialized at first usage, hence the behavior when you uncomment a.

Apparently, the typechecker manage to generalize at module boundary, I will not try to guess why since there is (Obj.)magic involved.

There is no obvious nice solution to this, since ocaml doesn't let you manipulate the row variable and doesn't specialize the type variable when you enter one branch, except when using gadt (that could deserve a feature request. It's related to this).

If you have only a few cases, or no complicated combination, you can try that:

module T : sig
  type foo = FOO
  type bar = BAR

  type _ generic =
    | Foo : int -> foo generic
    | Bar : int -> bar generic

  val map : (int -> int) -> 'a generic -> 'a generic

  val a : foo generic
  val b : bar generic
end = struct

  type foo = FOO
  type bar = BAR

  type _ generic =
    | Foo : int -> foo generic
    | Bar : int -> bar generic

  let map (type a) fn (x : a generic) : a generic = match x with
    | Foo x -> Foo (fn x)
    | Bar x -> Bar (fn x)

  let a = Foo 1 |> map succ
  let b = Bar 1 |> map succ
end

Answer 2

The only way a type maybe changed is when it is weak, and indeed, map inside your module has type (int -> int) -> (_[< generic ] as 'a) -> 'a, notice this _. So, that means, that before using your map you need to leave the T module:

let a = Foo 1 |> T.map succ

works as a charm.

What concerning a more general approach, that doesn't require any magic, then I would use the following. I will define explicitly a polymorphic type. The only difference is that since map is a mapping from 'a t to 'a t values a and b will have a more generic type 'a t.

module T : sig
  type generic =
    [ `Foo of int
    | `Bar of int ]

  type 'a t = 'a constraint 'a = generic
  val a : 'a t
  val b : 'a t
  val map : (int -> int) -> 'a t -> 'a t
end = struct
  type generic =
    [ `Foo of int
    | `Bar of int ]

  type 'a t = 'a constraint 'a = generic

  let map fn = function
    | `Foo x -> `Foo (fn x)
    | `Bar x -> `Bar (fn x)

  let a = `Foo 1 |> map succ
  let b = `Bar 1 |> map succ
end

But you may say, that this spoils the whole point, i.e., you want map to preserve type of its argument, so that if you call it with Foo it should return Foo. That just means that we should pick another constraint to our type, i.e., to use [< generic] instead of less general [generic]. In other words we are saying that our 'a is polymorphic to a subset of type generic, i.e., that it can instantiate to any type that is subset of generic. With this we can even hide our 'a t and show only generic type in our signature, thus achieving the original goal:

module T : sig
  type generic =
    [ `Foo of int
    | `Bar of int ]

  val map : (int -> int) -> generic -> generic

  val a : [`Foo of int]
  val b : [`Bar of int]
end = struct
  type generic =
    [ `Foo of int
    | `Bar of int ]

  type 'a t = 'a constraint 'a = [< generic]

  let map fn : 'a t -> 'a t = function
    | `Foo x -> `Foo (fn x)
    | `Bar x -> `Bar (fn x)

  let a : [`Foo of int] = `Foo 1 |> map succ
  let b : [`Bar of int] = `Bar 1 |> map succ
end