5
$\begingroup$

I'm studying some basic category theory in the context of type theory and came across the statement "simply typed lambda calculus is the internal language of cartesian closed categories". However terms and substitutions in the internal language of CCCs are the same data type, unlike in (traditional) STLC. Speaking in Agda, we have

π¹ : ∀ {Γ σ} -> Γ × σ ⊢ Γ
π² : ∀ {Γ σ} -> Γ × σ ⊢ σ
_[_] : ∀ {Γ Δ σ} -> Γ ⊢ σ -> Δ ⊢ Γ -> Δ ⊢ σ

where π¹ is supposed to be a substitution constructor and π² and _[_] are supposed to be term constructors.

This additional first-orderness allows to abstract over substitutions, so we can e.g. write (using de Bruijn indices)

I : ∀ {Γ σ} -> Γ ⊢ σ ⇒ σ
I = ƛ var 0

silly : ∀ {Γ Δ σ} -> Γ ⊢ Δ ⇒ σ ⇒ σ
silly = ƛ (I [ var 0 ])

I don't know what silly is, but it doesn't look like a regular lambda term to me.

So is the internal language of CCCs actually more expressive than STLC or am I misunderstanding something?

$\endgroup$
  • 1
    $\begingroup$ Substitution is a meta-level operation in STLC, but you seem to be talking about explicit substitutions? It would help if you explained a little what you're doing here. The "speaking in Agda" part is a bit too cryptic. $\endgroup$ – Andrej Bauer Mar 24 '16 at 7:28
  • $\begingroup$ @Andrej Bauer, nope, I would be satisfied by both meta-level substitutions and usual explicit substitutions. If I understand correctly, then the internal language of CCCs is this (after removing all categorical obfuscation). My question is: do I understand correctly and, if so, is this language more expressive than STLC? $\endgroup$ – user3237465 Mar 24 '16 at 10:36
5
$\begingroup$

Cartesian closed categories correspond to the simply typed lambda calculus with products. Your silly function is just $\lambda x.\lambda y.y$. If you want something that directly corresponds to the simply typed lambda calculus without implying products check out this paper by Bart Jacobs: Simply Typed and Untyped Lambda Calculus Revisited.

Let's instantiate your silly term and spell out what it looks like in type theoretic notation.

First, we're using _[_] at type $(\sigma \vdash \tau \Rightarrow \tau) \to (\Gamma\times\sigma\vdash\sigma) \to (\Gamma\times\sigma\vdash\tau\Rightarrow\tau)$. As a rule and placing in the terms, we get: $$\frac{z : \sigma \vdash \lambda y:\tau.y : \tau\Rightarrow\tau \qquad \Gamma, x:\sigma\vdash x:\sigma}{\Gamma,x:\sigma\vdash (\lambda y:\tau.y)[z\mapsto x]:\tau\Rightarrow\tau}$$ where $M[z\mapsto N]$ means "substitute $N$ for $z$ in term $M$". Of course, substituting for a variable that doesn't occur does nothing. So, in type theory, the above is (often by definition of substitution) equivalent to just $\Gamma,x:\sigma\vdash(\lambda y:\tau.y):\tau\Rightarrow\tau$. (Closely relatedly, weakening is also often transparent in type theory.) We then lambda abstract to get silly.

As a potential further insight, structural rules like $(\lambda y:\tau.M)[x\mapsto N] \equiv (\lambda y:\tau.M[x\mapsto N])$ with $y$ not free in $N$ come from naturality. This particular case comes from naturality of currying (if you spell it out, you'll see how the "$y$ not free in $N$" part is handled).

However, in this case it was a bit of a fluke that this worked out. In general, the second argument to _[_] should be a substitution, i.e. an arrow from contexts to contexts. In this code, a context is effectively represented by a left nested tuple (ending in an empty tuple). So if the second argument to _[_] does not return a left nested tuple, then _[_] will not behave like substitution. For example, the expression var 0 [ var 1 ] does not correspond to $$x:\sigma, y:\sigma \vdash x[x\mapsto y] : \sigma$$ like we might think, but rather to $$x:\sigma\times\sigma, y:\sigma \vdash \mathtt{snd}(x) : \sigma$$ This second interpretation is an artifact of this particular implementation that was exposed by failing to meet the precondition of _[_]. We would get the intended behavior had we written something like var 0 [pair unit (var 1)]. It would be cleaner and closer to typical STLC syntax to have _[_] take a vector of arrows that get tupled together in a left nested manner.

That this confusion between types and contexts is so easy is particular to CCCs. Most categorical semantics have a strict distinction between types and contexts; they live in separate categories. This is true of the semantics in the above mentioned Bart Jacobs paper. However, this conflation of types and contexts in CCCs makes it possible to discuss the categorical semantics without needing to introduce notions like indexed categories or fibrations.

$\endgroup$
  • $\begingroup$ Thanks for the reference, I'll check it. I know that CCC implies the corresponding lambda calculus has products. However I don't see how silly corresponds to ƛ ƛ var 0. Well yes, I can find the denotation of silly in the empty context, which is \x y. y, and quote it to get ƛ ƛ var 0, but I don't see how to directly interpret lambda abstracted substitution in the usual simply typed setting. $\endgroup$ – user3237465 Mar 24 '16 at 6:07
  • $\begingroup$ OK, my example is bad, because I is closed. I'm sorry for this extra confusion. Can you analyze silly : ∀ {Γ Δ σ} -> Γ ⊢ (Δ × σ) ⇒ σ ⇒ σ; silly = ƛ ƛ (var 0 [ var 1 ]) in the same way and say to what regular lambda term silly corresponds now? $\endgroup$ – user3237465 Mar 24 '16 at 10:40
  • $\begingroup$ It's not my notation — it's due to Church and de Bruijn. var 0 means (actually means) the rightmost variable and _[_] performs substitution. If I need to unwrap this primitives to get fancy sequences of π₁ and π₂ (and I can put ƛ or anything into substitutions) to understand the meaning of a term, then the semantics is simply broken. Which is rather convincing. Thank you for the elaboration. Though, it's still not clear to me whether this representation allows to define more terms than the usual one or not (I guess, not). $\endgroup$ – user3237465 Mar 24 '16 at 12:31
  • $\begingroup$ I don't have the said issue: I denote contexts by Γ and Δ and types by σ and τ and the type of _[_] is ∀ {Δ Γ σ} -> Γ ⊢ σ -> Δ ⊢ Γ -> Δ ⊢ σ as it should be. In this setting a substitution needn't be a sequence of terms, so var 1 is a valid substitution and that is the question: why is this called a categorical semantics of STLC, when it's a categorical semantics of something else? Anyways, if ψ is not a valid substitution, then t [ ψ ] shouldn't be a valid term. $\endgroup$ – user3237465 Mar 24 '16 at 14:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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