Erasable Dependent Types
Over a year ago I made a small implementation of a language with Erasable Dependent Types. The idea is that the majority of code utilizing types depending on values doesn’t actually need to exist at runtime; we can erase it. Proofs don’t need to exist at runtime, they only need to be evaluated in type checking. If this distinction is made by the programmer, i.e. utilizing special syntax, the interpreter can evaluate the source and generate new source with all of the runtime irrelevant information erased.
The classic example for showing off the power of dependent types is Vec. The length of a Vec in the type is a value being depended on. If we mark the length as irrelevant, we can erase the structure to one that is only depending on types:
// Vec takes in a Type and a Nat
// .Π means length is "irrelevant to computation"
val Vec: Π T: Type 0 -> .Π length: Nat -> Type 0
// the value of length is marked as irrelevant, so it can be erased
val ErasedVec: Π T: Type 0 -> Type 0
The rules for erasure are fairly simple. . denotes a term can be erased. Π, λ, and applications all have erased variants. We can recursively go through a program and take out the irrelevant terms.
Erasing a Π type requires replacing itself with its body while running the erasure on that body. If the body depends on a variable defined in an erased Π, it is an error (the program is trying to depend on erased information at runtime).
.Π x: X -> T ==> .T, erroring if .T depends on x
Erasing lambda expressions is similar; we can completely remove the lambda and variable and, if the body of the lambda depends on the erased variable, it’s an error.
.λ x: X => E ==> .E, erroring if .E depends on x
Application is a little more interesting because, now that our lambdas have been erased to their bodies, we can erase the parameter that was being passed in.
.(a b) ==> .a, erroring if .a requires a parameter
Combining these, we can describe the type of append for Vecs.
append :
Π T : Type 0 ->
.Π n : Nat ->
.Π m : Nat ->
Π _ : .((Vec T) n) ->
Π _ : .((Vec T) m) ->
.((Vec T) ((add m) n))
n and m are the lengths of the two Vecs we pass in. The returned Vec’s length is m + n, which is encoded in the type. Running erasure on this type results in a type similar to your standard append implementation.
erased_append :
Π T : Type 0 ->
Π _ : (Vec T) ->
Π _ : (Vec T) ->
(Vec T)
This becomes powerful for language implementation because erased_append is very easy to compile to machine code. If an erased value contains Π types whose variables aren’t used (indicated with _ above), they can be translated into normal function parameters. Π types whose variable is used must be Type 0 (these become normal generic type parameters that can be specialized through monomorphization).
For a time I was very interested in how dependent types could be efficiently compiled. Improvements have been made, but evaluation times for languages with dependent types are still slower than industry languages. I’m now leaning more towards Refinement Types or Liquid Types as a means of program verification, but I may continue this erasure experiment in the future.