In a dependently typed programming language is Type-in-Type practical for programming?

Question

In a language with dependent types you can have Type-in-Type which simplifies the language and gives it a lot of power. This makes the language logically inconsistent but this might not be a problem if you are interested in programming only and not theorem proving.

In the Cayenne paper (a dependently typed language for programming) it is mentioned about Type-in-Type that "the unstratified type system would make it impossible during type checking to determine if an expression corresponds to a type or a real value and it would be impossible to remove the types at runtime" (section 2.4).

I have two questions about this:

• In some dependently typed languages (like Agda) you can explicitly say which variables should be erased. In that case does Type-in-Type still cause problems?
• We could extend the hierarchy one extra step with Kind where Type : Kind and Kind : Kind. This is still inconsistent but it seems that now you can know if a term is a type or a value. Is this correct?

Answer 1

the unstratified type system would make it impossible during type checking to determine if an expression corresponds to a type or a real value and it would be impossible to remove the types at runtime

This is not correct. Type-in-type prevents erasure of proofs, but it does not prevent erasure of types, assuming that we have parametric polymorphism with no typecase operation. Recent GHC Haskell is an example for a system which supports type-in-type, type erasure and type-level computation at the same time, but which does not support proof erasure. In dependently typed settings, we always know if a term is a type or not; we just check whether its type is Type.

Type erasure is just erasure of all things with type Type.

Proof erasure is more complicated. Let's assume that we have a Prop universe like in Coq, which is intended to be a universe of computationally irrelevant types. Here, we can use some p : Bool = Int proof to coerce Bool-s to Int. If the language is consistent, there is no closed proof of Bool = Int so closed program execution never encounters such coercion. Thus, closed program execution is safe even if we erase all coercions.

If the language is inconsistent, and the only way of proving contradiction is by an infinite loop, there is a diverging closed proof of Bool = Int. Now, closed program execution can actually hit a proof of falsehood; but we can still have type safety, by requiring that coercion must evaluate the proof argument. Then, the program loops whenever we coerce by falsehood, so execution never reaches the unsound parts of the program.

Probably the key point here is that A = B : Prop supports coercion, which eliminates into computationally relevant universe, but a parametric Type universe has no elimination principle at all and cannot influence computation.

Erasure can be generalized in several ways. For example, we may have any inductive data type with a single constructor (and no stored data which is not available from elsewhere, e.g. type indices), and try to erase every matching on that constructor. This is again sound if the language is total, and not otherwise. If we don't have a Prop universe, we can still do erasure like this. IIRC Idris does this a lot.

Answer 2

I just want to add a note that I believe is related to the question. Formality, a minimal proof language based on self-types, is non-terminating. I was involved in a Reddit discussion about whether Formality can segfault. One way that could happen is if you could prove Nat == String, then cast 42 :: Nat to 42 :: String and then print it as if it was a string, for example. But that's not the case. While you can prove String == Int in Formality:

nat_is_string: Nat == String
  nat_is_string

And you can use it to cast a Nat to a String:

nat_str: String
  42 :: rewrite x in x with nat_is_string

Any attempt to print nat_str, your program will not segfault, it will just hang. That's because you can't erase the equality evidence in Formality. To understand why, let's see the definition of Equal.rewrite (which is used to cast 42 to String):

Equal.rewrite<A: Type, a: A, b: A>(e: Equal(A,a,b))<P: A -> Type>(x: P(a)): P(b)
  case e {
    refl: x
  } : P(e.b)

Once we erase the types, the normal form of rewrite becomes λe. λx. e(x). The e there is the equality evidence. In the example above, the normal form of nat_str is not 42, but nat_is_string(42). Since nat_is_string is an equality proof, then it has two options: either it will halt and become identity, in which case it will just return 42, or it will hang forever. In this case, it doesn't halt, so nat_is_string(42) will never return 42. As such, it can't be printed, and any attempt to use it will cause your entire program to hang, but not segfault.

So, in short, the insight is that self types allow us to encode the Equal, rewrite / subst, and erase all the type information, but not the equality evidence itself.