The Coq mailing list

[Neil Ghani <neil.ghani AT strath.ac.uk>]

I agree with much of this but not the generality. Look at sum types where the 
claimed generality doesn’t apply. 

A better idea is introduction and elimination are adjoint with the count 
being beta and the unit being eta ... this shows why eta is an expansion. And 
as an explanation, it delivers for sum types. Also works for empty types 

There’s some of this in my thesis 

Cheers
Neil  

Sent from my iPhone

> On 4 Oct 2019, at 17:27, Guillaume Brunerie 
> <guillaume.brunerie AT gmail.com>
>  wrote:
> 
> 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/