Type for "ways values can be different"

Question

I am looking for a concept in type theory that I am sure has probably been explored, but do not know the name behind.

Let's consider a ML-like language with product and sum types and a Hindley-Milner like type system. I'll use OCaml syntax.

I'm wondering about ways two different values can be different.

Use

My use case is writing "clearer" error messages in a xUnit-like library: if two values are different when they were expected to be equal, this can help build a clearer better message:

Before:

Values differ: expected {x = [1;2;3;4], y = "a long string"}, got {x = [1;2;3;3], y = "a long string"}

After:

Values differ: at position .x[3], expected 4, got 3.

(there might be a relation with functional lenses since we're ultimately constructing a lens to a smaller value which differs).

Product types

For example:

type p =
  { x : int
  ; y : string
  }

Equality can be defined as:

let equal a b =
  equal_int a.x b.x && equal_string a.y b.y

But it's also possible to reify the differences:

type delta_p =
  | Equal
  | Diff_x of int * int
  | Diff_y of string * string

let diff_p a b =
  if not (equal_int a.x b.x) then
    Diff_x (a.x, b.x)
  else if not (equal_string a.y b.y) then
    Diff_y (a.y, b.y)
  else
    Equal

(it might make sense to define a delta_int type as int * int to show that it is recursive)

Sum types

For a sum type there are more ways to differ: having a different constructor, or a different value

type s = X of int | Y of string

type ctor_s =
  | Ctor_X
  | Ctor_Y

type delta_s =
  | Equal
  | Diff_ctor of ctor_s * ctor_s
  | Diff_X of int * int
  | Diff_Y of string * string

let diff_s a b = match (a, b) with
  | X xa, X xb ->
    if equal_int xa xb then
      Equal
    else
      Diff_X (xa, xb)
  | (* Y case similar *)
  | X _, Y _ -> Diff_ctor (Ctor_X, Ctor_Y)
  | Y _, X _ -> Diff_ctor (Ctor_Y, Ctor_X)

What's the name of this concept? Where can I learn more about this?

Thanks!

Answer 1

I think you are looking for a typed variant of anti-unification. Anti-unification can be described as follows. First, suppose that we have a grammar of terms as follows:

t ::= () | (t, t) | C t | X 

Here, () and (t, t) denote units and pairs, C t is a term with a leading constructor, and X is a term variable, which could be substituted for any term.

The anti-unification problem says, if you give two terms t1 and t2, what is the least general term t such that there are substitutions s1 and s2 such that s1(t) = t1 and s2(t) = t2.

As a concrete example, given two terms

t1 = Cons(3, Cons(2, Cons(1, Nil)))
t2 = Cons(1, Cons(2, Cons(3, Nil)))

the anti-unification algorithm would return the anti-unifier

t = Cons(X, Cons(2, Cons(Y, Nil)))

because the substitutions s1 = [X:3, Y:1] and s2 = [X:1, Y:3] applied to t would give you t1 and t2 back. As an aside, we needed to specify "least general" because otherwise:

t' = Z 

with the substitutions s1 = [Z:t1] and s2 = [Z:t2] would do the trick.

Anti-unification was invented by Gordon Plotkin, and is a delightfully simple algorithm. Assume you have an injective name-generation function gen $: \mathrm{Term} \times \mathrm{Term} \to \mathrm{Var}$. Then we can find an antiunifier as follows

antiunify ()       ()         = ()
antiunify (t1, t2) (t1', t2') = (antiunify t1 t1', antiunify t2 t2')
antiunify (C t)    (C t')     = C (antiunify t t')
antiunify t        t'         = gen(t, t') -- default: t and t' dissimilar 

Augmenting this algorithm to return the two substitutions s1 and s2 I leave as an exercise.