The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Den fre 4 okt. 2019 kl 18:02 skrev 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 ~~> {}

This is indeed the rule that you want, but it is not a beta-reduction
rule, it is the eta-expansion rule for the unit type: every element u
of the unit type eta-expands to {}. In general, eta-expansion says
that an arbitrary element of the given type eta-expands to the
(unique) introduction rule applied to all the elimination rules, so in
the case of * it gives that u eta-expands to {}.

Best,
Guillaume

> 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/