codebje • last Monday at 3:47 AM

QTT is about clarity on erasing values rather than types, eg, if you define 'Vect n a' do you need to set aside space in the memory structure for a vector for 'n' or not. The types themselves are not represented. If, eg, you wanted to implement something that printed out its own type, like:

    vname : Vect n a -> String
    vname = "Vect " ++ show n ++ " " ++ nameOf a

Then (1) you'd be requiring "n" to be represented at run-time (so a QTT value of "unrestricted"), and (2) you'd need a type class to find "nameOf" for "a" when executing, because the actual type of "a" is gone. At runtime a type class means a table of methods passed to the function so it can call the right "nameOf" implementation.

      class Named a where
          nameOf a : String

      vname : Named a => Vect n a -> String
    ≡ vname : String -> Vect n a -> String

ChadNauseam • last Monday at 6:20 AM

In a sense, both you and the grandparent comment are right, although it will take some time for me to explain why.

1. There is an extremely strict sense of the concept of type erasure where the grandparent comment is right.

2. But in a practical sense of "I don't want these values in my binary", you are right.

So to resolve this confusion, it might be best to say exactly what dependent types are. "Dependent types", for all their mystery, are just a combination of three simple ideas:

1. What if you could: write functions that return types?

2. What if you could: say that the value of the input to a function can determine the type of the function's output?

3. What if you could: say that the value of the first thing in a tuple can determine the type of the second thing in the tuple?

For a concrete example, here is a very simple dependently typed function

    -- write functions that return types!
    pickType : Bool -> Type
    pickType True  = Nat
    pickType False = String

    -- the return type changes based on input!
    getValue : (b : Bool) -> pickType b
    getValue True  = 42
    getValue False = "hello"

You can see that there's nothing here inherently that requires any of the types or values to be kept around at runtime in order to use this function. In fact, here's how you might use it:

    useValue : Bool -> String
    useValue b = case b of
        True  => "The number is: " ++ show (getValue b)
        False => "The message is: " ++ getValue b

Once again, no type level terms need to be kept around at runtime to evaluate this. (Although you need a fairly intelligent typechecker in order to typecheck it.)

As nice as this is, the story gets a little less clean once you look at taking a dependent argument as a value. For example, we could not write this:

    takeValue : pickType b -> ()
    takeValue value = ()

If you try to write this, you would get a classic "using a variable before it's declared" error, because nowhere in this have we defined what `b` is. Instead you'd have to write

    takeValue : (b : Bool) -> pickType b -> ()
    takeValue b value = ()

The type system forces you to thread the value of b through your code (as a parameter) to any function that takes a pickType b. So while every type-level term is technically erased at runtime, in the strict sense that the compiler is not adding any extra stuff to the runtime that you didn't write yourself, the value will not truly be "erased" because you are forced to pass it everywhere even though you don't use it.

Obviously, this might be undesirable. So then you might further ask, "what are the situations in which we don't really need to enforce this constraint? when can a function take a dependent value without needing to know the values it depends on?"

That is where QTT comes in, as developed in Idris 2. Idris actually takes it a step further than we need for this conversation. For our purposes, all we need to do is say that there are two options for arguments into a function: arguments that are never used at runtime, and arguments that may or may not be used at runtime.

Let's say a function never uses one of its arguments. Then, clearly, as long as the compiler knows what that argument is, it doesn't have to actually write runtime code to pass it to the function. Let's allow the user of our made up language to prefix types that are never actually used at runtime with `0`.

    takeValue : (0 b : Bool) -> pickType b -> ()
    takeValue b value = ()

Now this should typecheck just fine because we're not actually using b, right? The compiler can easily see that.

And in fact, we can even pass b to another function as long as that function also marks its b as 0. (We know it will never actually get used so it's fine.)

    takeValuePrime : (0 b : Bool) -> pickType b -> ()
    takeValuePrime b value = takeValue b value

Now you can finally see where the "erasure" comes in. Any compiler can, as an optimization, erase values that are never used. And in dependently typed languages, it will often be the case that many terms are never actually used at runtime and can therefore be erased.