[Agda] Typed vs untyped lambda abstractions
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Aug 27 12:26:23 CEST 2012
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/
More information about the Agda
mailing list