# Type inequality constraints? **URL:** \ **Category:** Community\ **Tags:** types\ **Created:** [June 9, 2023, 6:25pm UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364 "2023-06-09T18:25:02Z")\ **Posts on this page:** 8\ **Page:** 1
**Author:** ![Paul\_A\_Steckler](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/paul_a_steckler/32/1763_2.png) [@Paul\_A\_Steckler](https://discuss.ocaml.org/u/Paul_A_Steckler)\ **Post date:** [June 9, 2023, 6:25pm UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/1 "2023-06-09T18:25:02Z")
OCaml lets you add equality constraints to type definitions: ```auto type t = A.t constraint t = B.t ``` Great, that means I can use instances of t in the same places I can use instances of B.t. But sometimes I want to know that types are incompatible. Does it make sense to have type inequality constraints: ```auto type t = M.t constraint t <> N.t ``` I want to be sure that I cannot use instances of t in contexts that allow instances of N.t. To implement this, compilation fails iff the analogous equality constraint would succeed. Any reason why this would not work? ---
**Author:** ![sim642](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/sim642/32/3597_2.png) [@sim642](https://discuss.ocaml.org/u/sim642)\ **Post date:** [June 10, 2023, 7:51am UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/2 "2023-06-10T07:51:43Z")
Not an expert on this, but I think it might be something like the following. The compiler failing to prove a type equality does not mean that the types are distinct. It could just mean that the type equality reasoning in the compiler is not powerful enough. So the compiler failing to do that doesn’t guarantee non-equality, making the whole inequality constraint thing completely useless. ---
**Author:** ![zbaylin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zbaylin/32/4047_2.png) [@zbaylin](https://discuss.ocaml.org/u/zbaylin)\ **Post date:** [June 11, 2023, 2:30am UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/3 "2023-06-11T02:30:53Z")
To expand upon @sim642’s comment, what would the expected behavior here be? ```ocaml type 'a t = unit constraint 'a <> int module type S = sig type t end module M : S (* makes [t] abstract externally *) = struct type t = int end let () : M.t t = () ``` Should this compile since `M.t` has not been proved to be equivalent to `int`? Or should it fail since values of `M.t` are also values of `int`? AFAIK both introduce undesirable behavior. If it _does_ compile, then you could end up with values of `'a t` with an unexpected underlying value/representation. Also, you could prove somewhere else that `M.t = int` (using type equality witnesses), which would would produce a contradiction. If it doesn’t compile, it breaks type abstraction (you know that `M.t = int`). ---
**Author:** ![yawaramin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yawaramin/32/3384_2.png) [@yawaramin](https://discuss.ocaml.org/u/yawaramin)\ **Post date:** [June 11, 2023, 4:08am UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/4 "2023-06-11T04:08:16Z")
What’s a use case example where you need an inequality constraint? ---
**Author:** ![Paul\_A\_Steckler](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/paul_a_steckler/32/1763_2.png) [@Paul\_A\_Steckler](https://discuss.ocaml.org/u/Paul_A_Steckler)\ **Post date:** [June 11, 2023, 4:31am UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/5 "2023-06-11T04:31:18Z")
The use case came up in some code I was working on. There were two types, call them M.t and N.t, which, using their original definitions, would have been allowed in a type equality constraint. Therefore, there were contexts where I could have used instances of either type. But the intention is that these types described different kinds of data, and I wanted to prevent confusion of the types. I redefined those types so they are not allowed in a type equality constraint, that is, compilation fails. It would be nice to have an affirmative indication that those types cannot be confused. ---
**Author:** ![art-w](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/art-w/32/4728_2.png) [@art-w](https://discuss.ocaml.org/u/art-w)\ **Post date:** [June 11, 2023, 10:53am UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/6 "2023-06-11T10:53:29Z")
**tl;dr:** Abstract types already give you the guarantee that you won’t accidentally unify the two types. To encode negation, the trick is to use the formulation `forall X, something_wrong -> X` which translates to “if you can construct a wrong term, then it implies I can deduce anything from it” (including more wrong stuff since I can choose what `X` stands for) For example, to prove that the type `int` and `string` are incompatible, we can write: ```ocaml type ('s, 't) eq = Refl : ('a, 'a) eq (* type 's and 't are equal, since 's='a and 't='a *) let impossible : type x. (int, string) eq -> x = function _ (* Any _ constructor representing the equality int=string *) -> . (* should be rejected statically by the typechecker as impossible *) ``` (The dot `.` is special notation to indicate an impossible pattern matching) The fact that we can define `impossible` this way is a proof that `int <> string`. If you try the same code with unifiable types, the typechecker will complain: ```ocaml let possible : type x. (int, Int.t) eq -> x = function _ -> . (* Error: This match case could not be refuted. Here is an example of a value that would reach it: Refl *) ``` But this approach will not work if your types are abstract! (as mentionned by @sim642) It’s possible for types to be equal behind the scene, and for that equality to still be accessible indirectly: ```ocaml module Test : sig module A : sig type t end module B : sig type t end val eq_ab : (A.t, B.t) eq end = struct module A = struct type t = string end module B = struct type t = A.t end let eq_ab = Refl (* at this point, we still have knowledge of the defintion of [A.t] and [B.t] *) end open Test let not_eq_ab : type x. (A.t, B.t) eq -> x = function _ -> . (* Error: This match case could not be refuted. Here is an example of a value that would reach it: Refl *) ``` If the typechecker accepted the definition of `not_eq_ab`, then we would run into problems since `not_eq_ab eq_ab` is actually possible! Sure, the types `A.t` and `B.t` are abstracted and hence not unifiable directly anymore… but we can locally reveal their equality by using `eq_ab`: ```ocaml let b_of_a : A.t -> B.t = fun a -> a (* error! *) let b_of_a : A.t -> B.t = fun a -> match eq_ab with Refl -> a (* ok! *) ``` In any case, abstract types are actually the way to go to ensure that you won’t confuse similar types in your function calls: they do give you the guarantee that the types will not unify out of the box (since you would have to work hard to un-erase the abstraction!) … and so in practice we don’t need to spend time trying to double-check what the typechecker will accept to unify 🙂 ---
**Author:** ![greedy](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/greedy/32/1388_2.png) [@greedy](https://discuss.ocaml.org/u/greedy)\ **Post date:** [June 11, 2023, 3:02pm UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/7 "2023-06-11T15:02:33Z")
When you have types for which you want to have the representation exposed, e.g.to avoid boxing overhead, but want the types to remain distinct even if the representation is the same, OCaml has a couple of options. I had this situation recently where I had table indexes that are represented as ints but didn’t want indexes into different tables to be confused. One is [private types](https://v2.ocaml.org/manual/privatetypes.html). With private types, clients of the module cannot directly create values but can coerce values into the underlying representation. Two private type aliases with the same representation still considered distinct from each other. For example, given ```auto module M : sig type t = private int val make : int -> t end = struct type t = int let make x = x end module N : sig type t = private int val make : int -> t end = struct type t = int let make x = x end ``` we get ```auto utop # M.make 3 = N.make 3;; Error: This expression has type N.t but an expression was expected of type M.t utop # (M.make 3 :> int) = (N.make 3 :> int);; - : bool = true utop # (* show that the representations are the same as int *) Obj.repr (M.make 3) = Obj.repr (N.make 3) && Obj.repr (M.make 3) = Obj.repr 3;; - : bool = true ``` Another is the `ocaml.unboxed` [built-in attribute](https://v2.ocaml.org/manual/attributes.html#ss%3Abuiltin-attributes). Here you can define a variant type with only one constructor but the representation will be exactly that of the constructor’s argument. Values of this type are built and used just the same as a regular variant type, the attribute just directs the compiler to use an optimized representation. This is the solution I chose in my program. This would look like ```auto type m = M of int [@@ocaml.unboxed] (* or type[@ocaml.unboxed] m = M of int *) type n = N of int [@@ocaml.unboxed] ``` and ```auto utop # M 3 = N 3;; Error: This variant expression is expected to have type m There is no constructor N within type m utop # (* show that the representations are the same as an int *) Obj.repr (M 3) = Obj.repr (N 3) && Obj.repr (M 3) = Obj.repr 3;; - : bool = true ``` ---
**Author:** ![Paul\_A\_Steckler](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/paul_a_steckler/32/1763_2.png) [@Paul\_A\_Steckler](https://discuss.ocaml.org/u/Paul_A_Steckler)\ **Post date:** [June 11, 2023, 6:32pm UTC](https://discuss.ocaml.org/t/type-inequality-constraints/12364/8 "2023-06-11T18:32:58Z")
Yes, I had chosen the unboxed-single-constructor approach to distinguish the types. The type inequality constraint would serve as proof and documentation that the types were not compatible.