The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

In the simply typed case, one might like eta-conversion for functions, 
products, and sums - three conversions in total.  In Coq 8.4, it looks like 
we now have eta for functions, and you're working on eta for products, so I'm 
wondering about the third conversion, eta for sums - is that possible or even 
sensible?

On Aug 28, 2012, at 9:34 AM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:

> 
> Le 28 août 2012 à 14:28, Adam Chlipala a écrit :
> 
>> On 08/28/2012 08:27 AM, Matthieu Sozeau wrote:
>>> η for (non-recursive) records will come along with a more efficient
>>> representation for projections which will not carry parameters anymore 
>>> (as in Agda too).
>>> 
>> 
>> This sounds a little scary from a trusted-code-base-size perspective.  
>> Does the proof checker need to get more complex to support your addition?
> 
> Nope, there is only less work to do. Compare:
> 
> In current Coq, when typechecking [proj params record]: infer the type of 
> [proj], typecheck params against the returned product type (and substitute 
> at the same time), typecheck record against the expected type. When I say 
> typecheck it means infer type and convert to the expected type.
> 
> Now we would have [record.(proj)]: Typecheck record and put in hnf: it has 
> to be of the form Ind params. Directly substitute (record, params) in the 
> (safe,trusted) type of the projection, you're done. Projections become a 
> particular kind of constants in this design and they're always applied to a 
> record. This makes the rest of the code (reduction, conversion) easier to 
> adapt than trying to keep projection names as regular constants and treat 
> the projection case as a subcase of regular application. Plus you'll never 
> see it reduced to [match foo with Record _ _ _ _ _ _ _ _ _ _ _ _ bar => bar 
> end].
> 
> Code-size-wise (of the TCB) it is a very small change.
> 
> Cheers,
> -- Matthieu