[Agda] Typed vs untyped lambda abstractions

[wren ng thornton]

On 8/25/12 12:19 PM, Guillaume Brunerie wrote:
> 2. What about syntactic study of type theory (confluence, strong
> normalisation, ...)? Is it easier with typed or untyped lambdas?

There's been an extremely long discussion on this topic. A theory with 
typed lambdas[1] is typically called "Church-like" or "à la Church"; 
whereas a theory with untyped lambdas[2] is typically called 
"Curry-like" or "à la Curry".

When dealing with weaker systems (e.g., simply-typed or 
Hindley--Milner--Damas), the standard formal properties of both versions 
coincide. One way to tell this is the case is because type inference is 
decidable. That is, after erasing all types and signatures (i.e., 
translate into the Curry-like system), we can fully reconstruct those 
types and signatures (i.e., translate back into the Church-like system).

However, as you move to more powerful systems, Curry-like systems go 
undecidable and lose other standard properties quicker than Church-like 
systems do. Which is why many theorists tend to prefer the Church-like 
when dealing with powerful systems. However, IMO, this Church-like bias 
means that Curry-like alternatives often aren't as well studied. So, 
while we have a fairly good understanding of the fine structure of 
boundaries for Church-like systems (e.g., consider the many systems of 
partial type inference for System F), the fine structure of boundaries 
for Curry-like systems are less well understood. And even though 
properties like decidable inference/checking fail more quickly in 
Curry-like systems, the Curry-like approach does have other nice 
semantic properties (e.g., sometimes we *want* (\x. x) to unify all 
identity functions) so they are still worthy of consideration and study.


[1] And other "mixing" of types into the term level; e.g., the explicit 
passing of types in System F.

[2] And no other "mixing" of types into the term level.

-- 
Live well,
~wren