[Agda] Typed vs untyped lambda abstractions

[Andreas Abel]

On 27.08.12 1:34 PM, Vladimir Voevodsky wrote:
> Let me ask a simple question related to this discussion. When one talks
> about "untyped application" and "untyped abstraction" does one actually
> mean that internally every object has to be kept as a part of a pair (o,
> T) where the second component is a type expression such that Gamma  |-
> o:T holds?

Depends what you want to do with object o.  If you just want the normal 
form, then you can ignore its type and context.  Evaluation needs to 
work without types, this is one of the design principles of Agda.

If you want to compile o into another language or do unification, you 
might be interested in its type and the types of its variables.  For 
top-level definitions the types are stored in the signature.  For 
subterms of terms defined at top-level, you can always reconstruct their 
type and context, since terms are beta-normal.  So, we do not need to 
store the tripel (Gamma, o, T) for every object o, since we can 
reconstruct Gamma and T.

Cheers,
Andreas

> On Aug 27, 2012, at 7:25 AM, Thierry Coquand wrote:
>
>>  Hello Andreas,
>>
>>
>>  You write
>>>
>>> When building a set-theoretic semantics, the type annotation at the
>>> lambda lets you build a set-theoretic function, so you can define the
>>> denotation of a term directly.
>>>
>>> For a categorical semantics, additional type annotation at
>>> application seems useful, see Streicher's PhD.
>>
>>  On the other hand, using Theorems 4.12 and 4.13 of Streicher's PhD
>> one can give categorical and set-theoretic semantics as well of the
>> calculus with "untyped application
>> and even with untyped function abstraction" , which is the calculus
>> used in Agda.
>> (Using these results one can lift any derivation of the untyped
>> calculus into a typed one in an essentially
>> unique way.)
>>
>>
>> Best regards,
>>
>> Thierry
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
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/