<p>I think you are looking for a typed variant of <a href="https://en.wikipedia.org/wiki/Anti-unification_(computer_science)" rel="noreferrer"><em>anti-unification</em></a>. Anti-unification can be described as follows. First, suppose that we have a grammar of <em>terms</em> as follows:</p>

<pre><code>t ::= () | (t, t) | C t | X 
</code></pre>

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

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

<p>As a concrete example, given two terms </p>

<pre><code>t1 = Cons(3, Cons(2, Cons(1, Nil)))
t2 = Cons(1, Cons(2, Cons(3, Nil)))
</code></pre>

<p>the anti-unification algorithm would return the anti-unifier </p>

<pre><code>t = Cons(X, Cons(2, Cons(Y, Nil)))
</code></pre>

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

<pre><code>t' = Z 
</code></pre>

<p>with the substitutions <code>s1 = [Z:t1]</code> and <code>s2 = [Z:t2]</code> would do the trick. </p>

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

<pre><code>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 
</code></pre>

<p>Augmenting this algorithm to return the two substitutions <code>s1</code> and <code>s2</code> I leave as an exercise.</p>

CC BY-SA 3.0
2017-09-22T07:52:21.387Z
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
CC BY-SA 3.0
2017-09-14T14:17:07.610Z
2017-09-14T14:17:07.610Z
Neel Krishnaswami
<p>I am looking for a concept in type theory that I am sure has probably been explored, but do not know the name behind.</p>

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

<p>I'm wondering about ways two different values can be different.</p>

<h3>Use</h3>

<p>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:</p>

<p>Before:</p>

<blockquote>
  <p>Values differ: expected <code>{x = [1;2;3;4], y = "a long string"}</code>, got <code>{x = [1;2;3;3], y = "a long string"}</code></p>
</blockquote>

<p>After:</p>

<blockquote>
  <p>Values differ: at position <code>.x[3]</code>, expected 4, got 3.</p>
</blockquote>

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

<h3>Product types</h3>

<p>For example:</p>

<pre><code>type p =
  { x : int
  ; y : string
  }
</code></pre>

<p>Equality can be defined as:</p>

<pre><code>let equal a b =
  equal_int a.x b.x &amp;&amp; equal_string a.y b.y
</code></pre>

<p>But it's also possible to reify the differences:</p>

<pre><code>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
</code></pre>

<p>(it might make sense to define a <code>delta_int</code> type as <code>int * int</code> to show that it is recursive)</p>

<h3>Sum types</h3>

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

<pre><code>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 -&gt;
    if equal_int xa xb then
      Equal
    else
      Diff_X (xa, xb)
  | (* Y case similar *)
  | X _, Y _ -&gt; Diff_ctor (Ctor_X, Ctor_Y)
  | Y _, X _ -&gt; Diff_ctor (Ctor_Y, Ctor_X)
</code></pre>

<p>What's the name of this concept? Where can I learn more about this?</p>

<p>Thanks!</p>

CC BY-SA 3.0
2017-09-14T12:18:11.597Z
A [zipper](https://wiki.haskell.org/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
CC BY-SA 3.0
2017-09-14T14:59:21.430Z
It was not really discussed in generality, but the use case reminds me of [The View from the Left](http://strictlypositive.org/vfl.pdf), 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
CC BY-SA 3.0
2017-09-22T07:51:10.313Z
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
<type-theory><functional-programming>
Type for "ways values can be different"
Étienne Millon
# Type for "ways values can be different"

(Asked by: username_0 on 2017-09-14)

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!

**Tags:** type-theory, functional-programming

> **Comments:**
> **username_1**: A [zipper](https://wiki.haskell.org/Zipper) is a "pointer" to a location. I don't know if anyone studied ways of nicely showing a zipper to the user.  
> **username_2**: It was not really discussed in generality, but the use case reminds me of [The View from the Left](http://strictlypositive.org/vfl.pdf), 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.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_3 on 2017-09-14. Score: 9 | Accepted answer

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.

> **Comments:**
> **username_0**: Thanks for the term (pun intended). That looks like it might be it. A typed algebra of "paths" like this would be great. Thanks!  

---

