Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.
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?