Type inequality constraints?

Community
1

OCaml lets you add equality constraints to type definitions:

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:

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?

2

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.

1 Like
3

To expand upon @sim642’s comment, what would the expected behavior here be?

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).

4

What’s a use case example where you need an inequality constraint?

5

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.

6

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:

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:

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:

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:

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 :slight_smile:

1 Like
7

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. 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

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

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. 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

type m = M of int [@@ocaml.unboxed] (* or type[@ocaml.unboxed] m = M of int *)
type n = N of int [@@ocaml.unboxed]

and

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
8

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.