# Comparing extensible variant type witnesses **URL:** \ **Category:** Learning\ **Created:** [January 5, 2022, 8:21pm UTC](https://discuss.ocaml.org/t/comparing-extensible-variant-type-witnesses/9110 "2022-01-05T20:21:01Z")\ **Posts on this page:** 4\ **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, 8:21pm UTC](https://discuss.ocaml.org/t/comparing-extensible-variant-type-witnesses/9110/1 "2022-01-05T20:21:01Z")
With a GADT of type witnesses, it is possible to write a function that tests for type equality: ```auto type (_, _) eq = Refl : ('a, 'a) eq type _ ty = Int : int ty | String : string ty let teq : type a b. a ty -> b ty -> (a, b) eq option = fun x y -> match (x, y) with | Int, Int -> Some Refl | String, String -> Some Refl | _, _ -> None ``` Is it possible to do something similar if `ty` is an _extensible_ variant, so that a user of the library can define their own types that can then be compared for equality? Of course there are limits on what sort of constructors a user could add and expect things to still work, e.g. if the user says ```auto type _ ty += Any : 'a ty ``` then I don’t expect there’s going to be any way to extend `teq` to deal with those. But if the user restricts themselves to simple constructors like `Int` and `String`, or perhaps parametrized ones for type formers like ```auto type _ ty += | List : 'a ty -> 'a list ty | Prod: 'a ty * 'b ty -> ('a * 'b) ty ``` can anything be done? I can think of two possibilities so far. One is to maintain a function like `teq`, or a list of them, in a mutable global variable, so that when users add constructors to `ty` they can “add clauses” to the match statement by adding new functions to this variable. This would be extra boilerplate for the user, but it would also exclude mistakes like `Any` since it wouldn’t be possible to write the corresponding clause. (Although it might require some cleverness to make this “extensible function” recursive enough to deal with `List` and `Prod`.) The other possibility I wonder about is ```auto type wrap = Wrap : 'a -> wrap let teq : type a b. a ty -> b ty -> (a, b) eq option = fun x y -> if Wrap x = Wrap y then Some (Obj.magic Refl) else None ``` On a [previous question](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/11) I learned that comparing elements of `wrap` for “structural equality” doesn’t see the types. But according to my current understanding, it seems that this comparison would still do the right thing on constructors such as `Int`, `String`, `List`, and `Prod`, since the type is reified in the constructors. Of course it would be wrong in the presence of a constructor like `Any`, in which case the `Obj.magic` would be actually ill-typed and cause all sorts of mayhem, so this is probably a Bad Idea in general. But in the interests of improving my understanding of OCaml, I’m curious whether this would at least work in the case when all constructors of `ty` are “good” ones. ---
**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:48pm UTC](https://discuss.ocaml.org/t/comparing-extensible-variant-type-witnesses/9110/2 "2022-01-05T20:48:01Z")
Types are never reified in constructors. Structural equality only compares blocks and immediate values, which for simple types is a sufficient notion of equality. Your `Obj.magic` version misbehaves as soon as two types may contain a block with the same tag or in presence of unboxed type. For instance `Wrap [1]` = `Wrap (1,0)`. In other words, `Obj.magic` is not part of the OCaml language: it should be seen as a tool for using OCaml as a compilation target from a more strongly typed language. ---
**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, 9:33pm UTC](https://discuss.ocaml.org/t/comparing-extensible-variant-type-witnesses/9110/3 "2022-01-05T21:33:01Z")
What I meant by “types are reified in constructors” is that the type `int` in `int ty` is represented by the constructor `Int`, and so on – the reification happens not at the language level, but by the user in the definition of the particular constructors. I don’t see how `Wrap [1] = Wrap (1,0)` is relevant, since I’m not applying `Wrap` to lists or pairs, only to elements of `'a ty` for different values of `'a`. Is there an example where it misbehaves using only the constructors `Int`, `String`, `List`, and `Prod`? ---
**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, 10:10pm UTC](https://discuss.ocaml.org/t/comparing-extensible-variant-type-witnesses/9110/4 "2022-01-05T22:10:23Z")
Sorry I read too fast. So yes, polymorphic comparison works fine within the same type because each constructor needs to be distinguishable from all others. With `Int`, `String`, `List` a,nd `Prod`, `Obj.safe` should be safe since each value maps to a single type with no type variables.