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

Question

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?

Answer 1

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.