The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi all,

I am stuck in thinking about the correspondence between simply typed lambda calculus (STLC) and cartesian closed category (CCC) but I am confused at some point. Since it is well-known, I appreciate any reference that makes every detail explicit.

By STLC, let's agree that it is defined by a unit type *, products _x_, and simple function spaces _->_. Its terms are defined in the typical way. Consider terms in STLC equivalent up to beta-eta reduction. Thus STLC forms a category with types as objects and functions between types as morphisms, and axioms are checked.

Now it remains to show that such STLC with beta-eta equivalence is a CCC. Consider a proof showing the unit type * is a/the terminal object of the category. It is required to show that there is a unique morphism/function from any type to * up to beta-eta equivalence. Consider the following two functions from * to *:

\x : *. x

and

\x : *. {}

It is clear that both definitions have type * -> *, but how on earth these two types are beta-eta equivalent? From all of the literature I checked, there is no reduction rule associated with terms of type *, while to actually make this two functions equivalent by beta-eta reduction, it seems to suggest the following rule:

G |- t : * => t ~~> {}

That is to add a beta rule which imposes the reduction of any term of type * to the unit element {} in one step. However, this doesn't make sense to me.

An alternative way to think about it is to assume functional extensionality and say that these two functions are extensionally equal. This feels much better, but that simply means the equivalence of morphisms/functions in STLC is no longer beta-eta equivalence but beta-eta equivalence + functional extensionality. It is more confusing if we think about type checkers, as it is clear that in that context we only consider reductions. Does that mean we tend to be more permissive when we try to think in a more mathematical setting?

How does this work? Is there any reference about the full details of this correspondence or I am just thinking about something weird?

Thanks,

Jason Hu

https://hustmphrrr.github.io/