[Agda] Typed vs untyped lambda abstractions
Vladimir Voevodsky
vladimir at ias.edu
Mon Aug 27 13:34:26 CEST 2012
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
More information about the Agda
mailing list