Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: programming

Topic: Coproduct in lambda calculus question

Henri Tuhola (Nov 04 2021 at 19:06):

I thought that coproducts are just Inl : a -> a+b, Inr : b -> a+b. With match: (a -> c) -> (b -> c) -> a+b -> c. Now I realised it's not precise.

Lambda calculus maps into cartesian closed category. The transform makes the scope explicit. Coproducts do not have input for the scope though.

What am I missing?

James Wood (Nov 05 2021 at 19:49):

Do I understand the question right that you're trying to reconcile the standard definition of a coproduct in a category with the syntactic constructs a λ-calculus with coproducts gives you? And which of these do you understand better?

Henri Tuhola (Nov 06 2021 at 10:02):

I understand both to some extent.

John Baez (Nov 06 2021 at 12:51):

You answered James' second question but not his first. (I'm always fascinated by how people don't answer questions, and how that makes communication harder - it's a bit of an obsession of mine.)

Henri Tuhola (Nov 06 2021 at 14:11):

It sounds like right description for these things. From now on I'll try to be more explicit with the limited knowledge I have.

John Baez (Nov 06 2021 at 14:13):

So you're trying to reconcile the standard definition of a coproduct in a category with the syntactic constructs a λ-calculus with coproducts gives you?

Henri Tuhola (Nov 06 2021 at 14:54):

Yes. On one side we get the morphisms (a -> a+b, b -> a+b) and the unique morphism (a+b->c) that can be constructed from morphisms (a->c, b->c).

On the other side we got (Inl, Inr) and match. This reconciles except that inside 'match' you have scope of variables.

Verity Scheel (Nov 06 2021 at 18:51):

You're saying that inside a match expression, you can access other variables bound in scope, but you don't see how that works categorically? I think it's just that if your scope consists of variables of types $v_1, v_2, \dots, v_n$, instead of $c$ (the goal type) you can consider $v_1 \to v_2 \to \cdots \to v_n \to c$ to be the new goal type, and now you have access to those variables in the match cases: $a \to (v_1 \to v_2 \to \cdots \to v_n \to c)$ and $b \to (v_1 \to v_2 \to \cdots \to v_n \to c)$. Technically this needs to be the internal hom, not an actual morphism in the category: $v_1 \implies v_2 \implies \cdots \implies v_n \implies c$. And typically we like to think of the bound context as represented by a product type $v_1 \times v_2 \times \cdots \times v_3$, to make it easier to work with as a single entity, instead of currying it like I did above. But I think that's the basic idea you are after.

Mike Shulman (Nov 06 2021 at 21:25):

It's true that type-theoretic sums have a stronger universal property than coproducts in a plain category. If the category has finite products, then this stronger universal property can be expressed by saying that it is a [[distributive category]]. Verity's argument explains why a cartesian closed category with coproducts is automatically distributive. Going the other way, you can express the stronger universal property in the absence even of finite products by working in a [[cartesian multicategory]].

Alex Gryzlov (Nov 08 2021 at 15:46):

John Baez said:

You answered James' second question but not his first. (I'm always fascinated by how people don't answer questions, and how that makes communication harder - it's a bit of an obsession of mine.)

Indeed, this is why I try to never ask two questions in a row without some sort of delimiter like bullet points!

Mike Shulman (Nov 08 2021 at 16:39):

https://motd.ambians.com/quotes.php/name/freebsd_fortunes_5/toc_id/1-0-6/s/597

John Baez (Nov 08 2021 at 17:03):

Never ask two questions in a business letter. The reply will discuss the one you are least interested, and say nothing about the other.

Robin Piedeleu (Nov 08 2021 at 17:39):

Coincidentally, a similar technique is also used by lawyers when taking the deposition of evasive witnesses!

John Baez (Nov 08 2021 at 18:28):

Yes, I've been in a jury and seen that!