The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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