<p>This is not a complete answer; it is a comment that got too large.</p>

<p>If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators <code>fst(e)</code> and <code>snd(e)</code>), there are no basically issues whatsoever. The reason it took so long to figure out is because it turns out to be more natural to do eta <em>expansions</em> rather than eta <em>reductions</em>.  See Barry Jay's <a href="http://math.ucr.edu/home/baez/qg-winter2007/virtues.ps" rel="noreferrer"><em>The Virtues of Eta Expansion</em></a>.</p>

<p>If you want products to have a pattern-style eliminator </p>

<pre><code>let (a,b) = e in t 
</code></pre>

<p>Then matters are more complex. The primary difficulty with pattern matching are the <em>commuting conversions</em>. That is, these calculi have the equation </p>

<pre><code>C[let (a,b) = e in t] === let (a,b) = e in C[t]
</code></pre>

<p>and figuring out (a)  which context <code>C[-]</code> to use and (b) how to orient this equation gets tricky. IMO, the state of the art for rewriting-style approaches are Sam Lindley's  <a href="http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf" rel="noreferrer"><em>Extensional Rewriting with Sums</em></a> and Gabriel Scherer's <a href="https://arxiv.org/pdf/1610.01213" rel="noreferrer"><em>Deciding Equivalence with Sums and the Empty Type</em></a>, both of which consider the typed lambda calculus with both products and sums.</p>

CC BY-SA 3.0
2017-09-07T08:21:27.483Z
2017-09-07T08:21:27.483Z
Neel Krishnaswami
<p>Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.</p>

<p><a href="http://www.sciencedirect.com/science/article/pii/S0304397508000571" rel="noreferrer">http://www.sciencedirect.com/science/article/pii/S0304397508000571</a></p>

<p>In some sense, a pattern is a tree of variables -- though I am just thinking of it as a nested tuple of variables, for example, ((x,y),z),(t,s)).</p>

<p>In the paper they showed that if the patterns are linear, in the sense that no variable in a pattern is repeated, then the rule</p>

<pre><code>(\p . m) n = m [n/p]
</code></pre>

<p>where p is a variable pattern and n is a tuple of terms with the exact same shape as p, is confluent.</p>

<p>I am curious if there are similar developments in the literature for the lambda calculus with patterns and the additional eta rule (expansion, reduction, or just equality).</p>

<p>In particular, by eta, I mean </p>

<pre><code>m = \lambda p . m p
</code></pre>

<p>More directly, I am curious what properties such a lambda calculus would have.  For example, is it confluent?</p>

<p>It forces the classifying category to be closed because it forces the property that</p>

<pre><code>m p = n p implies m = n 
</code></pre>

<p>By using the \xi-rule in between.  But perhaps something could go wrong?</p>

CC BY-SA 3.0
2017-08-30T13:16:38.663Z
Can you write put what eta rule you mean? Unless it's very strange you should be able to encode it using sums and make a simulation argument.
Max New
CC BY-SA 3.0
2017-08-31T10:12:57.463Z
@MaxNew: it looks like he's asking about the untyped calculus. Everything about patterns works perfectly with types (I oh-so-modestly suggest my own [*Focusing on Pattern Matching*](http://www.cl.cam.ac.uk/~nk480/pattern-popl09.pdf)), but untyped lambda calculus is different enough from typed LC (especially wrt eta) that I don't dare to answer without doing the proofs.
Neel Krishnaswami
CC BY-SA 3.0
2017-09-06T03:43:33.757Z
@MaxNew: What would encoding by sums entail?
Jonathan Gallagher
CC BY-SA 3.0
2017-09-06T03:48:31.557Z
@NeelKrishnaswami: I am actually interested in both.  I think I am nervous about having variables of a product type together with the eta rule.  I think this is done, for example, http://www.dicosmo.org/Articles/JFP96.pdf.  But if I'm mistaken, please correct me.  Then you have equalities like \lambda x .m x = m = \lambda (p,q) . m (p,q), for example.  Thanks for the link to your paper!
Jonathan Gallagher
<type-theory><lambda-calculus><typed-lambda-calculus><extensionality>
Eta expansion in the pattern lambda calculus
Jonathan Gallagher
# Eta expansion in the pattern lambda calculus

(Asked by: username_0 on 2017-08-29)

Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.
http://www.sciencedirect.com/science/article/pii/S0304397508000571
In some sense, a pattern is a tree of variables -- though I am just thinking of it as a nested tuple of variables, for example, ((x,y),z),(t,s)).
In the paper they showed that if the patterns are linear, in the sense that no variable in a pattern is repeated, then the rule
(\p . m) n = m [n/p]

where p is a variable pattern and n is a tuple of terms with the exact same shape as p, is confluent.
I am curious if there are similar developments in the literature for the lambda calculus with patterns and the additional eta rule (expansion, reduction, or just equality).
In particular, by eta, I mean 
m = \lambda p . m p

More directly, I am curious what properties such a lambda calculus would have.  For example, is it confluent?
It forces the classifying category to be closed because it forces the property that
m p = n p implies m = n 

By using the \xi-rule in between.  But perhaps something could go wrong?

**Tags:** type-theory, lambda-calculus, typed-lambda-calculus, extensionality

> **Comments:**
> **username_1**: Can you write put what eta rule you mean? Unless it's very strange you should be able to encode it using sums and make a simulation argument.  
> **username_2**: @MaxNew: it looks like he's asking about the untyped calculus. Everything about patterns works perfectly with types (I oh-so-modestly suggest my own [*Focusing on Pattern Matching*](http://www.cl.cam.ac.uk/~nk480/pattern-popl09.pdf)), but untyped lambda calculus is different enough from typed LC (especially wrt eta) that I don't dare to answer without doing the proofs.  
> **username_0**: @MaxNew: What would encoding by sums entail?  
> **username_0**: @NeelKrishnaswami: I am actually interested in both.  I think I am nervous about having variables of a product type together with the eta rule.  I think this is done, for example, http://www.dicosmo.org/Articles/JFP96.pdf.  But if I'm mistaken, please correct me.  Then you have equalities like \lambda x .m x = m = \lambda (p,q) . m (p,q), for example.  Thanks for the link to your paper!  

---

## 1 answers

### Answer by username_2 on 2017-09-07. Score: 7

This is not a complete answer; it is a comment that got too large.
If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators fst(e) and snd(e)), there are no basically issues whatsoever. The reason it took so long to figure out is because it turns out to be more natural to do eta expansions rather than eta reductions.  See Barry Jay's The Virtues of Eta Expansion.
If you want products to have a pattern-style eliminator 
let (a,b) = e in t 

Then matters are more complex. The primary difficulty with pattern matching are the commuting conversions. That is, these calculi have the equation 
C[let (a,b) = e in t] === let (a,b) = e in C[t]

and figuring out (a)  which context C[-] to use and (b) how to orient this equation gets tricky. IMO, the state of the art for rewriting-style approaches are Sam Lindley's  Extensional Rewriting with Sums and Gabriel Scherer's Deciding Equivalence with Sums and the Empty Type, both of which consider the typed lambda calculus with both products and sums.


---

