[Agda] Typed vs untyped lambda abstractions

[Andreas Abel]

Hello Guillaume,

On 25.08.12 6:19 PM, Guillaume Brunerie wrote:
> 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?

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.

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

If you consider typed equality, an annotation at the lambda is 
superfluous, since terms are always considered at their type.  For 
untyped equality, the situation is different, but it seems best to have 
annotation also at application (see recent work of Herbelin and Siles).

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

Internally, Agda's terms are in beta-normal form, meaning that the types 
of variables can be reconstructed directly from the types of the terms. 
  [See: bidirectional type checking]  Coq has been designed before 
bidirectional checking was popular and infers types.  The drawback of 
typed lambdas is additional redundancy, e.g. in the application rule you 
have

   t => (x : A) -> B
   u => A'
   A == A'
   -----------------
   t u => B[u/x]

so you get the type of the domain both from function t and argument u 
and have to check that both types coincide.

Typed lambdas lead to bigger internal representations, so currently, as 
long as we do not have proper sharing, it is not advisable to add type 
annotations to lambdas in Agda Internal Syntax.

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

Yes it is relatively easy when you have the type of the term; however, 
you have to propagate the type information to the lambda.

> I think I tried to find a suitable function in Agda's source code a few
> weeks ago, but I did not find anything.

What is the application you have in mind?

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/