Staging

[eashanhatti]

Getting my thought process for the design of the staging system down:

Staging allows us to express in the type system when a computation will take place. Implementing this is pretty simple, we index Type by a term of type Stage, which can be either 0 for run time or 1 for compile time (arbitrary names). Terms of kind Type 0 are evaluated at run time, while terms of kind Type 1 are evaluated at compile time.

if True : Bool : Type 0 then 33 else 34 -- run time `if`, eliminates a run time `Bool`
if True : Bool : Type 1 then 33 else 34 -- compile time `if`, eliminates a compile time `Bool`

However, we already run into a problem with this system, what if we make a stage of kind Type 0 - a stage evaluated at run time?

id : (s : Stage : Type 0) -> (A : Type s) -> A -> A
id _ _ x = x

id 1 String "foo"

This example doesn't make sense. "foo" is evaluated at compile time, hence the 1 passed to id, but the 1 is evaluated at run time. It will only be known at run time that "foo" should be evaluated at compile time. A fix that seems to work at first is just disallowing stages of kind Type 0:

id : (s : Stage : Type 1) -> (A : Type s) -> A -> A
id _ _ x = x

id 1 String "foo"

The s : Stage : Type 0 has been changed to s : Stage : Type 1. However, this actually doesn't work either. The 1 will be evaluated at compile time, but it will still be passed to id at run time. This narrows down the problem a bit: The problem is not that stages can be evaluated at run time, but rather that they can exist at run time at all. All that's need is for stages to be erased. Erasure it turns out, can be implemented in terms of the staging system. What we do is add another stage, let's call it 2, for terms that are evaluated at compile time and cannot be contained inside of a term that is not of stage 2. For pi types, if either the input or output types are stage 2, the pi type itself must be of stage 2. The same is true for sigma types and their components. The above example is now an ill-typed program as we need it to be, we have to write it like this (note that the Type 2 annotation on the function type is for clarity here, it could be inferred):

id : ((s : Stage : Type 2) -> (A : Type s) -> A -> A) : Type 2
id _ _ x = x

id 1 String "foo"

The function taking s as well as the argument passed for s will be evaluated at compile time, leaving a function of type (A : Type 1) -> A -> A for run time.

[eashanhatti]

Problem: The stage 1 doesn't work with functions.

record Foo : Type 0 where
    f : (Unit -> Unit) : Type 1

f is statically evaluated and thus inlined at all call sites. However, since Foo : Type 0, f must exist at run time, which cannot be the case if it is inlined - it doesn't make sense to hold a pointer to an inlined function.

[eashanhatti]

One solution is simply to disallow functions of stage 1, only allowing 0 and 2, but this seems not to work with stage polymorphism:

record Foo : (s : Stage) -> Type s where
    f : (Unit -> Unit) : Type s

foo : Foo 1 -- Would result in an error inside `Foo`'s declaration

You have to do something like below when working with multiple stage variables because stage 2 is restrictive - data of stage 2 can only be contained in other data of stage 2. When checking a declaration, all stage variables would be instantiated to 2 (An aside: Would this be the correct behavior?):

decide : Stage -> Stage -> Stage
decide 2 _ = 2
decide _ s = s

record (s1 s2 : Stage) -> Type s1 where
    f : (Unit -> Unit) : Type (decide s1 s2) 

This may or may not be relevant, not sure if the two problems are similar.