Extensible variants and functors

Learning
,
1

After seeing the interesting use of extensible variants in Add Type.Id by dbuenzli · Pull Request #11830 · ocaml/ocaml · GitHub,
I was interested in playing with them a bit more. I thought this would be true (in the REPL):

type id = ..
module F (X : sig type t end) = struct type id += Id end
module A = F(Int)
module B = F(Int);;
match A.Id with B.Id -> true | _ -> false;;

But in fact it is false. Even though this is true:

module F' (X : sig type t end) = struct type id = Id1 | Id2 end
module A' = F'(Int)
module B' = F'(Int);;
match A'.Id1 with B'.Id1 -> true | _ -> false;;

Actually I guess it makes sense, but I don’t fully understand what’s going on, so if somebody has more insight on why things must work this way, that would be nice !

1 Like
2

Each application of a functor yields a distinct module, even if you apply twice with the same parameter. Amongst other things:

  • Top-level side-effects are performed again.
  • Types/constructors are distinct.
1 Like
3

This seems like it’s true for generative functors (with an () argument) but not for the usual applicative functors in OCaml? Since F is applicative one would expect it to yield compatible types on applications to the same input. Am I mistaken?

My impression is that this applicativity does not hold in conjunction with extensible variants, which is something to be aware of.

1 Like
4

Applicative funtor does not ensure that new constructors are equals. It only ensures that type can be equal if you use the same module as argument (like A.id == B.id).

For instance, this code compile and we ensure that A.id == B.id.

type id = ..
module F (X : sig type t end) : sig type id += Id type id end = struct type id += Id type nonrec id = id end
module A = F(Int)
module B = F(Int)
let () = match A.Id with B.Id -> exit 0 | _ -> exit 1
type (_, _) eq = Refl : ('a, 'a) eq
let v : (A.id, B.id) eq = Refl
3 Likes
5

You have it right. For non-extensible constructors there is both type and constructor compatibility in the output of applicative functors. For example, the following code succeeds and prints 3:

module F(S: sig end) = struct type t = T of int end
module G1 = F(Int)
module G2 = F(Int)
let _ = match G1.T 3 with G2.T n -> Printf.printf "%d\n" n

However, since functors are executed just like functions each time they’re applied, and since extending an extensible variant performs an allocation, constructors of extensible variants resulting from distinct functor applications are not compatible. You can see the allocation in the “lambda” code generated by the compiler:

$ cat app.ml
type t = ..
module F(S: sig end) = struct type t += T end
$ ocamlopt -c  -dlambda app.ml 
(let
  (F/271 =
     (function S/276 is_a_functor
       (let (T/270 = (makeblock 248 "App.F(S).T" (caml_fresh_oo_id 0)))
         (makeblock 0 T/270))))
  (seq (setfield_ptr(root-init) 0 (global App!) F/271) 0))

Here the first makeblock allocates a fresh constructor each time the functor is applied. (The second makeblock is for the module itself).

3 Likes
6

Very clear. One way of looking at it could be that extensible types are ‘mutable types’, and functor application modifies them.