[Agda] Re: strict unit type
Andreas Abel
andreas.abel at ifi.lmu.de
Thu May 10 09:31:44 CEST 2012
On 10.05.12 1:11 AM, Vladimir Voevodsky wrote:
>
> 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.
Ah, sorry, my statement was imprecise. Of, course, you have many
different types for an object, but usually they share a common shape.
For instance, Pi-types are only convertible to types whose weak head
normal form is again a Pi-type. (And then domains and codomains are
convertible in turn.) Frederic Blanqui mentioned this injectivity of
Pi-type principle in an answer to your message on the TYPES list.
With your reductions you abandon the preservation of type shapes,
because a Pi-type can be equal to a base type like Pt. Your type
inference function
infer(Gamma |- e)
for a context Gamma and an o-term e has to take this into account. E.g.
if Gamma = x:Pt, y:Nat and you query
infer(Gamma |- x y)
then
infer(Gamma |- x) = Pt and infer(Gamma |- y) = Nat
and to justify
infer(Gamma |- x y) = Pt
you have to *expand* Pt = (Nat -> Pt). Of course, your algorithm does
not really need to expand, but to justify your algorithm, you cannot
work with a theory of reduction alone.
For practical reasons in Agda (as opposed to Coq and SML), we do not
work with inference alone. This is because terms from which you can
compute their type by an infer function contain a lot of redundant type
information (if inference is compositional). For instance, in application
infer(Gamma |- f) = Pi x:A.B infer(Gamma |- e) = A'
one needs to check A = A' before concluding
infer(Gamma |- f e) = B[e/x]
In bidirectional typing (see also Epigram, Haskell, Matita), type
information is propagated more flexibly. For instance, application
looks like
infer(Gamma |- f) = Pi x:A.B check(Gamma |- e : A)
----------------------------------------------------
infer(Gamma |- f e) = B[e/x]
Here, the domain type A of f is used to check the argument e, allowing e
to omit certain type annotations. E.g. if e = lambda y:A_1. e', then
the A_1 can be reconstructed from the A and does not have to be stored.
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/
More information about the Agda
mailing list