<p>I have developed this, but haven't yet published it in a more strucured/formal manner.</p>
<ul>
<li>&quot;Enhanced pattern unification&quot; <a href="https://wiki.portal.chalmers.se/agda/Main/AIMXXXIV" rel="noreferrer">abstract here</a>.</li>
<li><a href="https://github.com/AndrasKovacs/elaboration-zoo/tree/master/experiments/sigma-unification" rel="noreferrer">Demo implementation.</a></li>
<li><a href="https://www.youtube.com/watch?v=ioKwe5kvqdA" rel="noreferrer">Video recording</a>.</li>
</ul>
<p>You're absolutely on the right track when noting that <span class="math-container">$\eta$</span>-contraction is odd in pattern unification. An important point in the updated pattern unification algorithm is that we only do <span class="math-container">$\eta$</span>-expansion, similarly as in conversion checking. I give a short summary of the algorithm.</p>
<p>In the usual pattern unification, we create a partial inverse substitution from the spine of arguments. So e.g. <span class="math-container">$M\,x\,y = t$</span> yields <span class="math-container">$[x \mapsto a, y \mapsto b]$</span> where <span class="math-container">$a,\,b$</span> are fresh variables, and the solution  becomes <span class="math-container">$M \mapsto \lambda\,a\,b.\,t[x \mapsto a, y \mapsto b]$</span>. The <span class="math-container">$t$</span> substitution fails if <span class="math-container">$t$</span> depends on variables other than <span class="math-container">$x$</span> and <span class="math-container">$y$</span>; that's why it's a partial substitution.</p>
<p>The updated algorithm generalizes the spine inversion step, so that it can go under <span class="math-container">$\lambda$</span> and pairing. It turns out that this may require performing  pattern unification recursively during inversion.</p>
<p>For example, in <span class="math-container">$M\,(\lambda\,x\,y.\,f\,y\,x) = f$</span>, we want to &quot;invert&quot; the term <span class="math-container">$\lambda\,x\,y.\,f\,y\,x$</span> by mapping it to the fresh variable <span class="math-container">$a$</span>. Using informal notation, we need
<span class="math-container">$$(\lambda\,x\,y.\,f\,y\,x) \mapsto a$$</span>
this is decomposed to
<span class="math-container">$$\forall xy.\, f\,y\,x \mapsto a\,x\,y$$</span>
at which point we have the <em>recursive</em> pattern problem <span class="math-container">$f\,y\,x \mapsto a\,x\,y$</span>. So we perform the same kind of pattern unification on this problem, inverting the <span class="math-container">$y\,x$</span> spine to <span class="math-container">$[y \mapsto b, x \mapsto c]$</span>, yielding <span class="math-container">$[f \mapsto \lambda\,b\,c.\,a\,c\,b]$</span> as the result for the original spine inversion problem. Finally we get <span class="math-container">$M \mapsto \lambda\,a\,b\,c.\,a\,c\,b$</span>. Thus, instead of <span class="math-container">$\eta$</span>-contracting spine entries, we <span class="math-container">$\eta$</span>-expand in the solutions.</p>
<p>More generally, I conjecture that whenever <span class="math-container">$f$</span> is a definitional isomorphism in a decidable type theory with <span class="math-container">$\Pi$</span> and <span class="math-container">$\Sigma$</span>, the extended pattern unification algorithm solves <span class="math-container">$M\,(f\,x) = x$</span> as
<span class="math-container">$M \mapsto \lambda\,x.\,f^{-1}\,x$</span>. I haven't yet proven this formally, I'm fairly confident though. Unit types can be also handled, but in that case purely syntax-directed inversion is not enough, we need to track types (the same thing happens in conversion checking for unit <span class="math-container">$\eta$</span>).</p>

CC BY-SA 4.0
2021-12-28T22:52:30.490Z
"Intuitively, since definitional equality is decidable, definitional isomorphism should be also decidable" Really?
cody
CC BY-SA 4.0
2021-12-28T23:55:42.650Z
@cody I refined the wording. But I still don't see why the existence of definitional isos between given types would not be decidable. The language of def isos is very restricted compared to general terms. Haven't yet given an algorithm, I just think now that it's plausible.
András Kovács
CC BY-SA 4.0
2021-12-29T14:09:35.700Z
Can we make a precise statement about isos? Under the assumption that judgmental ("definitional") equality is decidable, it is clearly decidable whether $f$ and $g$ are (judgmental) inverses of each other. Now, given just $f$, where would a candidate $g$ come from?
Andrej Bauer
CC BY-SA 4.0
2021-12-29T14:50:11.897Z
@AndrejBauer edited, hopefully it's more precise now. Inverses come from the inversion algorithm.
András Kovács
CC BY-SA 4.0
2021-12-29T15:04:17.143Z
Thanks. Excuse my ignorance, but is "the inversion algorithm" something that is known under that name, or are you referring to something you developed and will be known in the future?
Andrej Bauer
CC BY-SA 4.0
2021-12-29T15:14:42.847Z
@AndrejBauer I borrowed "inversion" and "inverse substitution" as terminology from [here](https://sozeau.gitlabpages.inria.fr/www/research/publications/drafts/unification-jfp.pdf) and [here](http://www2.tcs.ifi.lmu.de/~abel/unif-sigma-long.pdf). The specific inversion algorithm which handles the more general isomorphisms was developed by me.
András Kovács
CC BY-SA 4.0
2021-12-28T20:57:56.683Z
2021-12-29T14:48:07.583Z
2021-12-29T14:48:07.583Z
András Kovács
<p>Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables.  Thus, for instance, an equation such as <span class="math-container">$M \,x\, y\, z = t$</span> can be solved by <span class="math-container">$M = \lambda x y z.t$</span>, assuming various side conditions hold (e.g. its RHS is in scope for <span class="math-container">$M$</span>, has a rigid head, and contains no occurrences of <span class="math-container">$M$</span>).  Unlike full higher-order unification, pattern unification has most-general unifiers and a fairly well-known algorithm to find them.</p>
<p>It seems to be fairly well-known that the &quot;universal variables&quot; occurring as arguments of an existential variable in a pattern unification equation can also be eta-expanded forms of variables.  For instance, <span class="math-container">$M \, x \, (\lambda u.y\, u)\,z = t$</span> is equivalent to <span class="math-container">$M \, x \, y \, z = t$</span> and has the same solutions.  Often this is handled in algorithms by eta-contracting the arguments of <span class="math-container">$M$</span>, which is slightly odd (since in most other contexts it seems better to treat eta-equivalence through expansion) but seems to mostly work.</p>
<p>However, what about something like <span class="math-container">$M \, x\, (\lambda uv. y\, v\, u)\, z = t$</span>?  Here the variable <span class="math-container">$y$</span> is not just eta-expanded, but its two arguments are swapped.  But in the presence of eta-conversion, knowing the value of <span class="math-container">$\lambda uv. y\, v\, u$</span> is equivalent to knowing the value of <span class="math-container">$y$</span>, and so the above equation has the solution <span class="math-container">$M = \lambda x y' z. t[y \mapsto (\lambda uv. y'\, v\, u)]$</span>.  Has anyone considered extending pattern unification to include cases like this?</p>

<type-theory><type-inference>
Swapping arguments of variables in higher-order pattern unification
Mike Shulman
# Swapping arguments of variables in higher-order pattern unification

(Asked by: username_0 on 2021-12-28)

Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables. Thus, for instance, an equation such as $M \,x\, y\, z = t$ can be solved by $M = \lambda x y z.t$, assuming various side conditions hold (e.g. its RHS is in scope for $M$, has a rigid head, and contains no occurrences of $M$). Unlike full higher-order unification, pattern unification has most-general unifiers and a fairly well-known algorithm to find them.

It seems to be fairly well-known that the "universal variables" occurring as arguments of an existential variable in a pattern unification equation can also be eta-expanded forms of variables. For instance, $M \, x \, (\lambda u.y\, u)\,z = t$ is equivalent to $M \, x \, y \, z = t$ and has the same solutions. Often this is handled in algorithms by eta-contracting the arguments of $M$, which is slightly odd (since in most other contexts it seems better to treat eta-equivalence through expansion) but seems to mostly work.

However, what about something like $M \, x\, (\lambda uv. y\, v\, u)\, z = t$? Here the variable $y$ is not just eta-expanded, but its two arguments are swapped. But in the presence of eta-conversion, knowing the value of $\lambda uv. y\, v\, u$ is equivalent to knowing the value of $y$, and so the above equation has the solution $M = \lambda x y' z. t[y \mapsto (\lambda uv. y'\, v\, u)]$. Has anyone considered extending pattern unification to include cases like this?

**Tags:** type-theory, type-inference

---

## 1 answers

### Answer by username_1 on 2021-12-28. Score: 20 | Accepted answer

I have developed this, but haven't yet published it in a more strucured/formal manner.

* "Enhanced pattern unification" [abstract here](https://wiki.portal.chalmers.se/agda/Main/AIMXXXIV).
* [Demo implementation.](https://github.com/AndrasKovacs/elaboration-zoo/tree/master/experiments/sigma-unification)
* [Video recording](https://www.youtube.com/watch?v=ioKwe5kvqdA).

You're absolutely on the right track when noting that $\eta$-contraction is odd in pattern unification. An important point in the updated pattern unification algorithm is that we only do $\eta$-expansion, similarly as in conversion checking. I give a short summary of the algorithm.

In the usual pattern unification, we create a partial inverse substitution from the spine of arguments. So e.g. $M\,x\,y = t$ yields $[x \mapsto a, y \mapsto b]$ where $a,\,b$ are fresh variables, and the solution becomes $M \mapsto \lambda\,a\,b.\,t[x \mapsto a, y \mapsto b]$. The $t$ substitution fails if $t$ depends on variables other than $x$ and $y$; that's why it's a partial substitution.

The updated algorithm generalizes the spine inversion step, so that it can go under $\lambda$ and pairing. It turns out that this may require performing pattern unification recursively during inversion.

For example, in $M\,(\lambda\,x\,y.\,f\,y\,x) = f$, we want to "invert" the term $\lambda\,x\,y.\,f\,y\,x$ by mapping it to the fresh variable $a$. Using informal notation, we need
$$(\lambda\,x\,y.\,f\,y\,x) \mapsto a$$
this is decomposed to
$$\forall xy.\, f\,y\,x \mapsto a\,x\,y$$
at which point we have the *recursive* pattern problem $f\,y\,x \mapsto a\,x\,y$. So we perform the same kind of pattern unification on this problem, inverting the $y\,x$ spine to $[y \mapsto b, x \mapsto c]$, yielding $[f \mapsto \lambda\,b\,c.\,a\,c\,b]$ as the result for the original spine inversion problem. Finally we get $M \mapsto \lambda\,a\,b\,c.\,a\,c\,b$. Thus, instead of $\eta$-contracting spine entries, we $\eta$-expand in the solutions.

More generally, I conjecture that whenever $f$ is a definitional isomorphism in a decidable type theory with $\Pi$ and $\Sigma$, the extended pattern unification algorithm solves $M\,(f\,x) = x$ as
$M \mapsto \lambda\,x.\,f^{-1}\,x$. I haven't yet proven this formally, I'm fairly confident though. Unit types can be also handled, but in that case purely syntax-directed inversion is not enough, we need to track types (the same thing happens in conversion checking for unit $\eta$).

> **Comments:**
> **username_2**: "Intuitively, since definitional equality is decidable, definitional isomorphism should be also decidable" Really?  
> **username_1**: @cody I refined the wording. But I still don't see why the existence of definitional isos between given types would not be decidable. The language of def isos is very restricted compared to general terms. Haven't yet given an algorithm, I just think now that it's plausible.  
> **username_3**: Can we make a precise statement about isos? Under the assumption that judgmental ("definitional") equality is decidable, it is clearly decidable whether $f$ and $g$ are (judgmental) inverses of each other. Now, given just $f$, where would a candidate $g$ come from?  
> **username_1**: @AndrejBauer edited, hopefully it's more precise now. Inverses come from the inversion algorithm.  
> **username_3**: Thanks. Excuse my ignorance, but is "the inversion algorithm" something that is known under that name, or are you referring to something you developed and will be known in the future?  
> **username_1**: @AndrejBauer I borrowed "inversion" and "inverse substitution" as terminology from [here](https://sozeau.gitlabpages.inria.fr/www/research/publications/drafts/unification-jfp.pdf) and [here](http://www2.tcs.ifi.lmu.de/~abel/unif-sigma-long.pdf). The specific inversion algorithm which handles the more general isomorphisms was developed by me.  

---

