[Agda] Typed vs untyped lambda abstractions

[Guillaume Brunerie]

Hello,

I have a few questions about typed vs untyped lambda abstractions.

More specifically,
1. I have the impression that categorical semantics of type theory is
easier with typed lambdas, because for example the term "\ x -> x" could be
a lot of different functions but "\ x : A -> x" is the identity function of
A.
Is that right? Do you have references of papers discussing categorical
semantics of type theory with untyped lambdas?

2. What about syntactic study of type theory (confluence, strong
normalisation, ...)? Is it easier with typed or untyped lambdas?

3. Why does Agda use untyped lambdas (internally)? Are there any advantages
or drawbacks? I think that Coq uses typed lambdas, but I don't know if
there is a difference from an implementation or user-friendliness point of
view.

4. Using Agda's source code, is it easy to add type annotations to lambdas?
In other words, if I have a term in Agda's internal syntax (of type
Agda.Syntax.Internal.Term, I think), how do I translate it to a term in a
lambda calculus with typed lambdas?
I think I tried to find a suitable function in Agda's source code a few
weeks ago, but I did not find anything.

Thank you,

Cheers,
Guillaume
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120825/d277b6c0/attachment.html