Structural equality for GADTs

If two elements of a GADT compare as structurally equal, are any existential types they contain also necessarily equal? And if so, is there any way to access this fact?

For example, I would like to write something like this:

type (_, _) eq = Eq : ('a, 'a) eq
type wrap = Wrap : 'a -> wrap

let cmp : type a b. a -> b -> (a, b) eq option =
 fun x y -> if Wrap x = Wrap y then Some Eq else None

but of course the typechecker complains on the last line that Eq doesn’t have the correct type (a, b) eq. But in that branch of the if statement we have Wrap x = Wrap y; does that mean the types a and b are necessarily actually equal? And if so, is there any way to convince the typechecker of it (e.g. would Obj.magic be safe)?

No, as = just compares the untyped runtime representation of values. For example: Wrap 0 = Wrap None.



Whoa! That’s creepy.

So I guess if I want to meaningfully compare elements of GADTs for structural equality, I need to make sure the runtime representation contains sufficient information to determine the existential types.

I was legitimately surprised by this. Why = works like this makes sense after thinking about it a bit, but it’s IMO quite regrettable that an operation with such semantics is named as it is (the underlying runtime function compare_val is a much more sensible name).

Notable also that ='s documentation is not explicit about the consequences of “untyped structural comparison”. Most of the admonitions re: being cautious with = have focused on the pitfalls of comparing mutable values, but the above example is IMO much more disconcerting.

I am not sure if this example is really surprising? The type wrap is black box that throws away all type information. I think that it makes sense that using the equality on such a black box type does not care about the type information that has been purposefully erased

1 Like

I don’t agree that wrap “throws away all type information”: at compile-time, the type information is present and can be extracted. So I think it’s not unreasonable for cemerick and me to be surprised that the type information is ignored by =. Maybe for someone who is used to thinking about types as something that are erased at runtime this isn’t surprising, but I would expect that plenty of programmers don’t think that way unless forced to. And even given that types are erased at runtime, there’s no a priori reason to expect that None and 0 would have the same runtime representation.

In any case, I do think it would be helpful to mention this in the documentation.

No, wrap really throws away all type information immediately and definitively. Once you have constructed a value of type Wrap x, there is no way to use x ever again outside of the built-in functions that look at the runtime memory representation:

let black_box = Wrap 0
let error =
  let Wrap x = black_box in

Error: This expression has type $Wrap_'any
but an expression was expected of type 'a
The type constructor $Wrap_'any would escape its scope

Well, maybe you can make that argument about wrap in particular.
But existential types in general are not completely thrown away,
otherwise they wouldn’t be good for anything. So I think it makes
sense to have an intuition about them that extends to wrap.

Existential types are always “throw away” from the point of the view of the outside world , that’s why you need either companion functions:

type showable = Show: 'a * 'a -> unit : showable

or a type witness

type 'a typ = Int: int typ | Float: float typ
type dyn = Dyn: 'a typ * 'a -> dyn

to make the existentially quantified contents useful.

In the first case, the = functions is not supported due to the presence of functions.
More interestingly, in the second case, the polymorphic = equality will distinguish all the types that can be distinguished with the help of the type witness which seems like the right behavior.
In other words, It is only constructors that have arguments with completely erased type that end up with an untyped comparisons.


To be clear, my surprise was due to my forgetting that nullary variant constructors are represented as simple integers at runtime. e.g. 0 and None really do have exactly the same in-memory representation:

utop # Marshal.to_bytes 0 [];;
- : bytes =
Bytes.of_string "\132\149\166\190\000\000\000\001\000\000\000\000\000\000\000\000\000\000\000\000@"
─( 13:51:57 )─< command 1 >───────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # Marshal.to_bytes None [];;
- : bytes =
Bytes.of_string "\132\149\166\190\000\000\000\001\000\000\000\000\000\000\000\000\000\000\000\000@"

and just to demonstrate the generality of nullary variant representations:

# type t = Foo | Bar;;
type t = Foo | Bar
# 0 = Obj.magic Foo;;
- : bool = true
# 1 = Obj.magic Bar;;
- : bool = true

“Equality” is of course a loaded, imprecise concept in most languages, but even so, I think surprise in this case is warranted even if one groks e.g. existentials. = “tests for structural equality”, but that really overstates things; what it actually does is much more akin to memcmp than anything most people would call “equality”.

P.S. Maybe the claim of “tests for structural equality” would make more sense if all values were boxed?
P.P.S. I wonder if there are other optimizations / in-memory representations that produce surprising outcomes?

I don’t think a programmer should be required to “remember that nullary variant constructors are represented as simple integers at runtime” in order to understand the behavior of a fundamental language construct like equality. Knowledge of runtime representations may be useful for performance optimization, but isn’t it part of the purpose of a high-level language like OCaml to insulate the programmer from having to think about such things in order to write correct code?

Perhaps your expectation of polymorphic comparison is greater than it deserves? Polymorphic comparison is generally avoided by OCaml programmers and I imagine very few consider it a “fundamental language construct”. Rather it’s more of a cheap hack that can often save you a little time.

1 Like

I fundamentally agree with you, but also, the knowledge that polymorphic comparison operators are fraught has been widely known for some time (e.g. I think this from 2008 is the canonical post: Jane Street Tech Blog - The perils of polymorphic compare), and AFAIK all of the community standard libraries remove polymorphic comparisons by default.

Of course, compatibility requires that the thing at Stdlib.(=) remain as it is. I do think it’s reasonable to suggest that the documentation be clarified, maybe in light of modern understandings/expectations of “equality”.

The issue is that there is no simple, universal and easily computed notion of equality for all possible types: for some types, we are interested to a bit-by-bit identity equality, for some other type, we are only interested in equality module some isomorphism and not the finer implementation detail. Similarly, for some type equality is generally undecidable.

Structural equality is just a well behaved equality function for simple types, and not really a language construct.

If you want an intuition of what is wrap, and according to your mathematical background, wrap is just the terminal object of the Set category, i.e. a singleton. Hence the only reasonable way to define the equality on this type is with fun _ _ -> true. Here, as with many other types, the built-in polymorphic (=) (based on structural runtime representation of values) is just leaking implementation details.

Your existential type wrap is just structurally, from a typing point of view, equivalent to this one:

module type Wrap : sig
  type t
  val wrap : 'a -> t
end = struct
  type t = int
  let wrap _ = 1

The fact is that polymorphic (=) (that can’t be defined in the language) or what you’re trying to do, do not compare values of the codomain wrap (which is a singleton) but values of the domain of the Wrap constructor.

Can you obtain that intuition as a special case of an intuition about arbitrary GADTs with existential types?

For sure, take your definition:

type wrap = Wrap : 'a -> wrap

In the graph of Set category, the constructor Wrap is just the label of the arrow that maps any type to the terminal object wrap. Up to isomorphism, your type wrap could be replaced by unit and the arrow is just the polymorphic function ignore. The intuition is similar to the one I gave here with cone and co-cone for type base dynamic dispatch.

The constructor Wrap just says there is a map from every object to wrap, which says much less than that wrap is terminal. Any nonempty set admits a map from every other set.

If wrap were the colimit of the identity functor of Set – or even, by a standard lemma, if these maps to wrap were natural with respect to all functions and the special case Wrap : wrap -> wrap were the identity – then yes, wrap would be terminal. But for a general GADT it doesn’t even make sense to ask for it to be a colimit of something, or for the constructors to be natural. Consider for instance

type show = Show : 'a * ('a -> string) -> show

where the input operation 'a * ('a -> string) is not even a functor, so it doesn’t make sense to ask about its colimit or for a transformation defined on it to be natural.

The only thing I can think of that does make sense in general is a coproduct. But then wrap would be the coproduct of all the objects of Set, which is not the terminal object.

(To be sure, a coproduct of all the objects of Set doesn’t exist for size reasons. But the same argument applies in a category of modest sets in realizability, etc.)

Wrap says more than that, it states that there is only one way to inject a type in wrap and that it’s the same for any type. From the theorem for free Wadler’s paper, only constant function have this type inj : 'a -> foo for any type foo. (look at this blog post from Bartosz Milewski). In other words, the image by inj of any type is exactly the same singleton subtype of foo (it was the singleton {1} in my example above with foo = int). There is absolutely no way to distinguish two values of type wrap if you only use functions that you can define in the language. Try to implement a function with this type wrap -> wrap -> bool (without any built-in), and you’ll find there is only two : the two constant ones, and the one constantly equal to true is the equality relation on wrap, i.e it’s a singleton.

For instance, I can implement this interface with unit:

module Top_unit : sig
  type t
  val wrap : 'a -> t
end = struct
  type t = unit
  let wrap = ignore

and you agree that unit is a singleton. But there is no way to distinguish two types with such an interface and there’s only one injection between two of them.

module type Top = sig
  type t
  val wrap : 'a -> t

(* now we compare two distinct implementations *)
module M (Top1 : Top) (Top2 : Top) = struct
  (* the only way to produce a value of type Top2.t is
     to use the `wrap` function from `Top2` *)
  let top1_to_top2 : Top1.t -> Top2.t = fun x -> Top2.wrap x

 (* for the same reason there is only one injection in the other sense *)
  let top2_to_top1 : Top2.t -> Top1.t = fun x -> Top1.wrap x

To me it really looks like a terminal object: for any given type 'a there is only one arrow with domain 'a and codomain Top.t, namely the function Top.wrap.

With type show it’s different. You could have write:

type show = Show : ('a -> string) * 'a -> show

with GADT constructors OCaml uses an uncurry notation, but you should think of it as:

type show = Show : ('a -> string) -> 'a -> show

and so for any type 'a you have a family of injection from 'a to show indexed by conversion function of type 'a -> string. Hence, for a given type the injection is not unique, and it’s not even the same for two distinct types. And if you see it as a module type:

module type Show = sig
  type t
  val show : ('a -> string) -> 'a -> t

the simplest implementation is to use type t = string and show f x = f x. In other words, your type show is equivalent to string. The fact that you can implement this interface with a GADT is just an implementation details.

1 Like

Parametricity results like “theorems for free” are about syntax, not semantics. So wrap is still not the terminal set, it’s just that you can’t distinguish it from the terminal set in syntax.

I do see your point about parametricity. But I think your notion of “intution” is different than mine. (-: