[Agda] Re: strict unit type

[Andreas Abel]

On 30.04.12 3:36 PM, Vladimir Voevodsky wrote:
>>> PS There is another non-confluent situation with a ->   tt for a
>>> : Pt which does not require dependent sums namely \lambda x:T, f
>>> x where f : T ->   Pt reduces both to f and to \lambda x:T tt .
>>> Both non-confluences can be taken care of by additional
>>> reductions in particular the reduction \prod x:T, Pt ->   Pt for
>>> the example with \lambda.
>>
>> Such a reduction is unhealthy except in the situation where \prod
>> is a "for all" that does not leave marks on the term level.
>
> Well, that was my first thought as well but I am not so sure now. It
> does make it necessary to do some type checking before beta-reduction
> but anyhow the reduction such as a ->  tt for objects of the unit
> type makes reduction context dependent. I have not checked all the
> details yet but it is possible that one can preserve confluence and
> normal form and still have reductions which change the
> sum/prod-structure of type expressions.

I agree that this can likely be modeled, i.e., terms and types can be 
interpreted in a way that these reductions become identities. 
Partially, this is done in Werner et al.'s proof irrelevant model of the 
CIC.

However, I am not so convinced that reduction is the right method in 
this case.  For instance, subject reduction fails unless you work on 
equivalence classes of types.  A more "semantic" approach seems more 
fitting, from my experience.  Also, from the implementor's perspective 
such reductions complicate the picture.  For instance, the problem

   tt : \prod x:T. Y(x)    with Y a meta-variable

cannot be decided at the spot, but has to wait for the solution of Y. 
Also, then a term has many types, which makes type inference more 
complicated.

In Agda, if you have to supply a term of type \prod x:T. Pt, you can 
always just write _ (for a fresh meta-variable).  Eta-expansion then 
fills in the term for you

   _ --> \x:T. _ --> \x:T. tt

That seems to do the job.

> PS From the point of view of a user who wants to construct/verify
> proofs the more identifications are recognized by the underlying
> system the better.

I agree, this is why I have been working on (proof) irrelevance for Agda.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/