5

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).

2
  • I just read the "note about the real system" ... you could just use objects for that, you know ? It seems rather fitting. :)
    – Drup
    Apr 13, 2015 at 17:26
  • I gave that a try too. It solves this problem but it introduces other issues (I really want to treat these items as pure data and pattern-match on them in multiple places). Apr 16, 2015 at 8:51

3 Answers 3

3

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
1
  • Thanks for the link. I tried it with a GADT earlier, but for the real program I really need subsets. Apr 12, 2015 at 17:36
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
4
  • Your second example looks interesting but doesn't compile for me (4.02.1): The second variant type does not allow tag(s) ``Bar. I would like to have map be polymorphic though; a and b were just for testing. Apr 12, 2015 at 17:33
  • well, it is polymorphic, try it yourself, let a : [Foo of int] = Foo 1 |> T.map succ, this is outside the module, and it can be applied to a subset of generic without loosing refutability of this subset
    – ivg
    Apr 12, 2015 at 17:56
  • What version of OCaml are you using? I tried with 4.01 and 4.02 and it refused to compile it: File "test.ml", line 21, characters 26-44: Error: This expression has type generic t but an expression was expected of type [ ``Foo of int ] The second variant type does not allow tag(s) ``Bar Apr 12, 2015 at 19:27
  • I'm using ocamlmerlin, and it accepts this code. Indeed, when I compiled this with ocaml compiler it shows the same. Looks like that we've found bug in ocamlmerlin, will look at it closer...
    – ivg
    Apr 12, 2015 at 19:44
1

Why do you require the signature of the map function to be

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

It makes little sense to me as you are trying to restrict the “openness” of the variant types. It seems to me that there are two natural signatures for the map function. The first possibility is

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

so that map f can be applied on a subtype of generic and produces a value which is naturally embedded into any supertype of generic. The second possibility is

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

where map f can be applied on any supertype of generic but will only process variants in generic and presumably leave other values unchanged.

The first signature can be implemented as

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

  val map : (int -> int) -> [< generic ] -> [> generic ]
end = struct
  type generic =
    [ `Foo of int
    | `Bar of int ]

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

The second signature can be implemented as

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

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

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

It makes little sense to me to write a function whose range is a closed variant, one should use a classical sum type instead. Maybe it is even impossible to write such a function, which specialists may confirm.

5
  • I've added a bit at the end of the question explaining the real use-case. Apr 13, 2015 at 8:15
  • Open variants are not really types, the careful wording of the manual is “a variant tag does not belong to any type in particular, the type system will just check that it is an admissible value according to its use”. The type … -> [< generic] would mean that the function produces values that can only processed by functions accepting the variants cases defined as generic but not more. I do not understand why you want enforce this restriction or why you use open variants as they are designed to circumvent this restriction! Apr 13, 2015 at 8:50
  • If the next function takes [< ``Foo | ``Other] as 'b then there's no problem; it will just use 'b = ``Foo. Apr 13, 2015 at 10:02
  • If the function returns [> ‘Foo | ‘Other ] it says “I can talk to every one understanding ‘Foo and ‘Other” and I understand you want it to say “I can talk to every one understanding ‘Foo and ‘Other and nothing more”. I think there is just a confusion resulting from thinking that [> …] and [> …] notations denote classical types, which they don't. The signature you actually want to implement is probably val map : (int -> int) -> [< generic] -> [> generic]. Apr 13, 2015 at 12:16
  • I don't, because the next function cannot handle all the types in generic. e.g. think about get_foo () |> map incr |> save_foo, where save_foo cannot handle Bar. The ideal type might be [> 'a] but that seems unnecessarily complicated. Apr 13, 2015 at 12:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.