<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**: @username_1: 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**: @username_1: What would encoding by sums entail?  
> **username_0**: @username_2: 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*](http://math.ucr.edu/home/baez/qg-winter2007/virtues.ps).

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*](http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf) and Gabriel Scherer's [*Deciding Equivalence with Sums and the Empty Type*](https://arxiv.org/pdf/1610.01213), both of which consider the typed lambda calculus with both products and sums.


---

