coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ryan Wisnesky <ryan AT cs.harvard.edu>
- To: Matthieu Sozeau <mattam AT mattam.org>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] eta(?) conversion in records?
- Date: Tue, 28 Aug 2012 12:18:40 -0400
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
- [Coq-Club] eta(?) conversion in records?, Jason Gross, 08/18/2012
- Re: [Coq-Club] eta(?) conversion in records?, Andreas Abel, 08/27/2012
- Re: [Coq-Club] eta(?) conversion in records?, Matthieu Sozeau, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Adam Chlipala, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Matthieu Sozeau, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Adam Chlipala, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Ryan Wisnesky, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Andrew Cave, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Matthieu Sozeau, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Adam Chlipala, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Matthieu Sozeau, 08/28/2012
- Re: [Coq-Club] eta(?) conversion in records?, Andreas Abel, 08/27/2012
Archive powered by MHonArc 2.6.18.