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: community: general

Topic: Lambda Calculus and CCCs

Alexander Gietelink Oldenziel (Nov 23 2020 at 22:04):

The internal language of Cartesian closed categories is the simply typed lambda calculus. In this correspondence the unit of the adjunction $$_ \times A \vdash (_)^A$$ is the evaluation map $ev:Y^A \times A \to Y$ corresponds to beta reduction.
What does the unit map $Y\to (Y\times A)^A$ correspond to?
In Set it takes $y\in Y$ and sends it to the map $a \mapsto (y,a)$ I think.

Dan Doel (Nov 23 2020 at 22:11):

(Some) programmers call that type the 'state monad', and it's the unit, which takes a pure value of $y : Y$ and sends it to the computation that yields $y$ and doesn't use or modify the state.

But it depends how you're interpreting things a bit.

James Wood (Nov 23 2020 at 22:25):

Alexander Gietelink Oldenziel said:

the unit of the adjunction ${-} \times A \vdash ({-})^A$ is the evaluation map $ev:Y^A \times A \to Y$ corresponds to beta reduction.

This doesn't sound right. Morphisms should correspond to terms of STλC, so that a morphism $A → B$ is exhibited by a term $M$ such that $x : A ⊢ M : B$. β-reduction only comes in when we want to define equality on these terms (and we'll want η-expansion, too). Then we can say that the category STλC has as objects the simple types (generated from some base types) and as morphisms either a quotient of the well typed terms (under α, β, and η rules) or the well typed βη-normal forms (and both could have typed constants added).

Dan Doel (Nov 23 2020 at 22:32):

One way of doing the correspondence doesn't have a $×$ type for instance. The Cartesian product is only used for the context structure. An arrow $A × B × C × \ldots → X × Y × Z × ...$ corresponds to many terms $A,B,C,... = Γ ⊢ X \quad Γ ⊢ Y \quad Γ ⊢ Z \quad ...$

In this scenario, the object $(Y × A)^A$ is going to be used as its equivalent $Y^A × A^A$, and so $Y → (Y × A)^A$ is going to be a two-term in context $Y$, the first of which is $y : Y ⊢ λ a. y \ :\ A → Y$ and the second is $y : Y ⊢ λa. a \ : \ A → A$. So it's just some random thing that isn't called out as very interesting normally.

Dan Doel (Nov 23 2020 at 22:34):

In this methodology $ev$ is $f : Y→A, y : Y ⊢ f y : A$

Dan Doel (Nov 23 2020 at 22:39):

I suppose you might say it's not completely uninteresting, because those are two of the SKI combinators (K and I). Or K and backwards K depending on how you want to read it.