# Structural equality for GADTs **URL:** \ **Category:** Learning\ **Tags:** gadt\ **Created:** [January 5, 2022, 7:39am UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104 "2022-01-05T07:39:20Z")\ **Posts on this page:** 20\ **Page:** 1
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 7:39am UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/1 "2022-01-05T07:39:20Z")
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: ```auto 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)? ---
**Author:** ![nojb](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/nojb/32/519_2.png) [@nojb](https://discuss.ocaml.org/u/nojb)\ **Post date:** [January 5, 2022, 8:23am UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/2 "2022-01-05T08:23:25Z")
> [@viritrilbia](#): > > does that mean the types `a` and `b` are necessarily actually equal? No, as `=` just compares the untyped runtime representation of values. For example: `Wrap 0 = Wrap None`. Cheers, Nicolas ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 8:32am UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/3 "2022-01-05T08:32:52Z")
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. ---
**Author:** ![cemerick](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/cemerick/32/1383_2.png) [@cemerick](https://discuss.ocaml.org/u/cemerick)\ **Post date:** [January 5, 2022, 4:18pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/4 "2022-01-05T16:18:23Z")
> [@nojb](#): > > No, as `=` just compares the untyped runtime representation of values. For example: `Wrap 0 = Wrap None` . 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`](https://github.com/ocaml/ocaml/blob/c8730eef5971dc6c2de1518d1c9107eba3bd5617/runtime/compare.c#L91) is a much more sensible name). Notable also that [`=`'s documentation](https://ocaml.org/api/Stdlib.html#1_Comparisons) 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. ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [January 5, 2022, 5:09pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/5 "2022-01-05T17:09:03Z")
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 ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 5:28pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/6 "2022-01-05T17:28:15Z")
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. ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [January 5, 2022, 5:49pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/7 "2022-01-05T17:49:47Z")
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: ```ocaml let black_box = Wrap 0 let error = let Wrap x = black_box in x ``` > Error: This expression has type $Wrap\_'any > but an expression was expected of type 'a > The type constructor $Wrap\_'any would escape its scope ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 6:04pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/8 "2022-01-05T18:04:36Z")
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`. ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [January 5, 2022, 6:15pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/9 "2022-01-05T18:15:32Z")
Existential types are always “throw away” from the point of the view of the outside world , that’s why you need either companion functions: ```ocaml type showable = Show: 'a * 'a -> unit : showable ``` or a type witness ```ocaml 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. ---
**Author:** ![cemerick](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/cemerick/32/1383_2.png) [@cemerick](https://discuss.ocaml.org/u/cemerick)\ **Post date:** [January 5, 2022, 7:53pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/10 "2022-01-05T19:53:38Z")
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: ```auto 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: ```auto # 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? ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 8:02pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/11 "2022-01-05T20:02:39Z")
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? ---
**Author:** ![rgrinberg](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/rgrinberg/32/40_2.png) [@rgrinberg](https://discuss.ocaml.org/u/rgrinberg)\ **Post date:** [January 5, 2022, 8:30pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/12 "2022-01-05T20:30:06Z")
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. ---
**Author:** ![cemerick](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/cemerick/32/1383_2.png) [@cemerick](https://discuss.ocaml.org/u/cemerick)\ **Post date:** [January 5, 2022, 8:32pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/13 "2022-01-05T20:32:00Z")
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](https://blog.janestreet.com/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”. ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [January 5, 2022, 8:59pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/14 "2022-01-05T20:59:38Z")
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. ---
**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\ **Post date:** [January 5, 2022, 9:54pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/15 "2022-01-05T21:54:09Z")
> [@viritrilbia](#): > > So I think it makes > sense to have an intuition about them that extends to `wrap` . 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: ```ocaml module type Wrap : sig type t val wrap : 'a -> t end = struct type t = int let wrap _ = 1 end ``` 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. ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 10:07pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/16 "2022-01-05T22:07:51Z")
Can you obtain that intuition as a special case of an intuition about arbitrary GADTs with existential types? ---
**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\ **Post date:** [January 5, 2022, 10:13pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/17 "2022-01-05T22:13:45Z")
For sure, take your definition: ```ocaml 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](https://discuss.ocaml.org/t/ad-hoc-polymorphism-and-usability/9059/17) with cone and co-cone for type base dynamic dispatch. ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 5, 2022, 10:31pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/18 "2022-01-05T22:31:46Z")
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 ```auto 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.) ---
**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\ **Post date:** [January 6, 2022, 3:11pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/19 "2022-01-06T15:11:24Z")
> [@viritrilbia](#): > > The constructor `Wrap` just says there is a map from every object to `wrap` , which says much less than that `wrap` is terminal. `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](https://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free/)). 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`: ```ocaml module Top_unit : sig type t val wrap : 'a -> t end = struct type t = unit let wrap = ignore end ``` 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. ```ocaml module type Top = sig type t val wrap : 'a -> t end (* 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 end ``` 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: ```ocaml type show = Show : ('a -> string) * 'a -> show ``` with `GADT` constructors OCaml uses an uncurry notation, but you should think of it as: ```ocaml 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: ```ocaml module type Show = sig type t val show : ('a -> string) -> 'a -> t end ``` 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. ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [January 6, 2022, 4:42pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/20 "2022-01-06T16:42:44Z")
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. (-: [Next page](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104.md?page=2)