2
$\begingroup$

In the untyped lambda calculus (with variables, abstraction and application as the only constructors), we have a "pair" construct, given by $(a, b) = \lambda x, x a b$. The projections are then $\pi_i = \lambda x_1 x_2, x_i$ and there is a product function $ \langle f, g \rangle = \lambda x, (f x, g x)$.

TL; DR; Do we also have something like that, but for a copair/disjunction/union?

In the essay Relating Theories of the lambda-calculus, Scott constructs (from page 418) a category $R$, consisting of all idempotent functions $A \circ A = A$. To each of the objects $A$, we can attach a 'set of elements', consisting of all the terms $a$ such that $A a = a$. This category has binary products $A \times B = \langle A \circ \pi_1, B \circ \pi_2 \rangle $, with a set of elements consisting of $x$ that are equal to $(a, b)$ for some element $a$ of $A$ and $b$ of $B$. Note that $A \times B$ is exactly the product function of the two projections onto $A$ and $B$.

My main question here is: does this category have binary coproducts $A \sqcup B$? Is there a type $X$ such that $X x = x$ means "$A x = x$ or $B x = x$" or something like that? Can we construct an idempotent "Bool" which has exactly two elements?

I noticed that we can create injection functions $\iota_1 = \lambda a x_1 x_2, x_1 (A a)$ and $\iota_1 = \lambda b x_1 x_2, x_2 (B b)$ from $A$ and $B$ into a coproduct, and that given functions $f: A \to C$ and $g: B \to C$, we can combine them into a sum function $[f, g] = \lambda x, x f g$. However, when I try to take $A \sqcup B = [\iota_1, \iota_2]$, just like with the binary product, I sadly get something which is not idempotent. Is what I am trying to do just impossible?

$\endgroup$
2
  • 1
    $\begingroup$ I thought about it for a week. I can't even find a terminal object without adjoining constants; I'm not sure if we can have 2 = 1 + 1 if we can't even have 1. Excellent question, thanks. $\endgroup$
    – Corbin
    Apr 2 at 19:14
  • 1
    $\begingroup$ @Corbin Thank you for your time. The terminal object is already given by Scott. It is given by a "constant" function: $ \lambda x_1 x_2, x_2 $. There is no initial object by the way, because there are always multiple possible functions (for example, all the constant functions) to $ \lambda x_1, x_1 $. $\endgroup$ Apr 3 at 12:48

1 Answer 1

2
$\begingroup$

The usual way to encode coproducts is as:

$$ι_1\ x = λk_1\ k_2.\ k_1\ x \\ ι_2\ y = λk_1\ k_2.\ k_2\ y$$

Matching is then, as you said, $[f,g]= λs.\ s\ f\ g$.

The obvious problem with idempotence is that you didn't dualize the product. For the product you wrote:

$$A × B = \langle A \circ π_1, B \circ π_2 \rangle$$

The dual of this would be:

$$A + B = [ι_1 \circ A, ι_2 \circ B]$$

However, this still isn't idempotent. For arbitrary $z$, we get:

$$(A+B)((A+B)z) = z (ι_1 \circ A) (ι_2 \circ B) (ι_1 \circ A) (ι_2 \circ B)$$

There's no obvious way for the repeated applications to interact and reduce unless $z$ is already a 'good' value from the set we haven't yet established.

The obvious difference is that $A×B$ always produces something like a pair, but whether the above $A+B$ produces something like a disjunct is entirely up to $z$. So, we should try to take that out of $z$'s hands. If we imagine what $A+B$ does in a more standard light, we'd get:

$$(A+B)z = \mathsf{match}\ z\ \mathsf{with} \\ ι_1 x → λl\ r. l\ x \\ ι_2 y → λl\ r. r\ y$$

So, an idea is to instead write this as:

$$(A + B)z = λ l\ r. \mathsf{match}\ z\ \mathsf{with} \\ ι_1 x → l\ x \\ ι_2 y → r\ y$$

Or, in just lambda terms:

$$(A+B) = λs\ l\ r. [l \circ A, r \circ B]\ s$$

Now this is idempotent:

$$\begin{align} (A&+B)((A+B)z) \\ &= (A+B)(λ l\ r. [l \circ A, r \circ B]\ z) \\ &= λ l\ r. (λ l'\ r'. [l' \circ A, r' \circ B]\ z)\ (l \circ A)\ (r \circ B) \\ &= λ l\ r. [l \circ A \circ A, r \circ B \circ B]\ z \\ &= λ l\ r. [l \circ A, r \circ B]\ z \end{align}$$

The two constructors also satisfy $(A+B)(ι_i x) = ι_i x$ as long as $x$ satisfies the relevant equation. For example:

$$\begin{align} (A &+ B)(ι_1\ x) \\ &= λ l\ r. (λ l'\ r'. l' x) (l \circ A) (r \circ B) \\ &= λ l\ r. l (A x) \\ &= λ l\ r. l x \\ &= ι_1 x\end{align}$$

I don't know if it satisfies all the properties you want, but perhaps it will work out better.

$\endgroup$
5
  • $\begingroup$ This seems to work. Why didn't I think of this myself‽ $\endgroup$ Apr 3 at 23:25
  • $\begingroup$ It works up to the last part. I only wasn't able to show uniqueness of the coproduct arrow. I.e. I was not able to show that for $ f: A \to C $ and $ g: B \to C $, for all arrows $ h: A + B \to C $ such that $ h \circ \iota_1 = f $ and $ h \circ \iota_2 = g $, we have $ h = C \circ [f, g] $. One of the complications here is that the product arrow $ \langle f, g \rangle $ satisfies $ \langle f, g \rangle \circ a = \langle f \circ a, g \circ a \rangle $, but the coproduct arrow does not satisfy (afaik) $ a \circ [f, g] = [a \circ f, a \circ g] $. $\endgroup$ Apr 5 at 7:33
  • $\begingroup$ Yeah, it may just not work out. One other thing I noticed is that if you do this for booleans, you get $\mathsf{Bool}\ b = λ f\ t. b\ f\ t$. But then $\mathsf{Bool}\ b = b$ is just the eta rule that all lambda terms are expected to satisfy. $\endgroup$
    – Dan Doel
    Apr 5 at 15:19
  • $\begingroup$ Oh, that is not what we wanted indeed. I also realized that Paul Taylor in his dissertation proved that the category of retracts cannot have coproducts (if we have a "nontrivial" lambda-calculus. I.e., if there are at least two distinct lambda-terms): paultaylor.eu/domains/recdic.pdf, 1.5.12, the corollary. $\endgroup$ Apr 5 at 17:31
  • $\begingroup$ However, thank you for taking the time to think about this. $\endgroup$ Apr 5 at 17:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.