[Agda] Re: strict unit type
Vladimir Voevodsky
vladimir at ias.edu
Thu May 10 01:11:48 CEST 2012
On May 1, 2012, at 3:51 AM, Andreas Abel wrote:
> 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 the system which I am trying to write up there is a typing function on terms i.e. for any o-term X (object like term) and any function \Gamma assigning t-terms (type-like terms) to the free variables in X there is a simply computed t-term \tau_{\Gamma}(X) which, if everything happened to be derivable gives a canonical representative to the type of X.
The fact that there can be many t-terms which are definitionally equal to \tau_{\Gamma}(X) seems unavoidable in any system with universes.
Vladimir.
More information about the Agda
mailing list