Theoretical Computer Science
typed-lambda-calculus
Updated Sat, 25 Jun 2022 20:38:14 GMT

Can you always throw away the types when evaluating lambda expressions?


As I understand it, in the simply typed lambda calculus you can type-check your terms, then throw away all the types and do the evaluation exactly as if it was the untyped lambda calculus. Is that always the case or do some typing systems require you to know the types when evaluating terms?




Solution

It is not always the case. Systems where this is possible are called "Curry style," and systems where it is not possible are called "Church style." The general idea is that in Curry style systems, the types are a mechanism for reasoning about pre-existing structure. The types just help us make sense/keep track of ways of using said structure. In a Church style system, the types are a necessary part of specifying the structure/behavior of the terms.

A relatively simple example of something Church style is type classes in Haskell. For instance, we have:

read "45" :: forall t. Read t => t

as a most general type. We could also instantiate it to:

read "45" :: Int
read "45" :: Double

However, completely eliminating types leaves something under specified. In the first case, the Read t constraint indicates that the behavior we get for any instantiation of t will depend by cases on t. When instantiated to Int, we get 45, and when instantiated to Double we get 45.0, and these are not represented identically in some underlying untyped system. To elaborate this into an untyped system, we need to not just erase types, but add arguments that correspond to how the types influence the actual meaning of the term. A common way of doing this for type classes is dictionary passing, which gives something like:

\readDict -> read readDict "45"
read readDictInt "45"
read readDictDouble "45"

A more complicated example is homotopy type theory. It's typical to imagine that type/universe arguments to functions in dependent type theory still enjoy erasure, because you cannot write programs that do case analysis on them. However, this is no longer really the case when identity types for them have non-trivial computational content. Given a family:

P : T -> Type

and an identity:

e : Id T t u

we can obtain:

subst P e : P t -> P u

which may have meaningful computational content, because in general it could correspond to any sufficiently nice function from P t to P u. For instance, we might have P t = and P u = , and subst P e is some enumeration of all integers.

This information is not trivial, and it at least seems to indicate that we cannot just erase things like P because they are 'type level'. It doesn't make sense to say that we can go from:

(\P ... -> ...) : (P : T -> Type). ...

to:

(\ ... -> ...) : ...

becuase P is where we get the enumeration of the integers. So, even if we're going to 'erase' types, we need to do so in a way where the untyped level has extra information plumbed through it corresponding to the types, similar to the type class example above. In this case, we need to retain a function that maps identities in T to functions between the right types.





Comments (3)

  • +0 – This is not what is usually meant by the Church-Curry distinction. Church vs Curry is a property of a semantics (defined over typing derivations or untyped terms) and sometimes it is shown that. Church style and Curry style semantics are equivalent: tidsskrift.dk/brics/article/view/20167 — May 14, 2022 at 12:45  
  • +0 – The question, and my answer, are about semantics. Can you give an untyped meaning to typed terms in a way that the meaning doesn't depend on the types (and thus, can be given by naively erasing types)? In my examples, then answer is, "no." — May 14, 2022 at 16:30  
  • +0 – I'm not saying your answer is wrong, I'm just objecting to your use of "Church"/"Curry" terminology. What I meant is that "Church"/"Curry" is a property of the definition of a semantics, and "Church" style semantics doesn't imply that it isn't possible to write an alternative, equivalent semantics that doesn't depend on the structure. — May 17, 2022 at 16:16