[Agda] Typed vs untyped lambda abstractions

[Andreas Abel]

On 27.08.12 1:25 PM, Thierry Coquand wrote:
>> 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.)

Yes.  Agda's terms are not "inherently untyped" since each subterm can 
be assigned a unique type.  I have no access to Streicher's thesis here, 
but for constructing a semantics, this route seems feasible

   "untyped" terms with their types --reconstruction-->
   "typed" terms                    --interpretation-->
   semantics

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/