[Agda] Re: strict unit type

[Andreas Abel]

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/