Type for “ways values can be different”

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)


Thanks!

• A zipper is a "pointer" to a location. I don't know if anyone studied ways of nicely showing a zipper to the user. – Andrej Bauer Sep 14 '17 at 12:18
• It was not really discussed in generality, but the use case reminds me of The View from the Left, section 7, where they make a verified type checker that reports precise difference between expected and general type. Figure 15 has the Isnt type that is analogous to your use case. – Max New Sep 14 '17 at 14:59
• Thanks for the pointers. It seems to me that zippers are more about "moving" left and right than focusing, but that's also an effect they have. That seems pretty related to view patterns indeed. – Étienne Millon Sep 22 '17 at 7:51

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.

• Thanks for the term (pun intended). That looks like it might be it. A typed algebra of "paths" like this would be great. Thanks! – Étienne Millon Sep 22 '17 at 7:52