[Agda] Typed vs untyped lambda abstractions

[Vladimir Voevodsky]

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?

Vladimir.


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
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120827/9830d1e0/attachment.html