Did some cooking with Edwin yesterday, and we came up with an ExTT-like way of separating phases. The idea is to annotate context entries and the typing judgment with a level number (low numbers are more dynamic), with

\Rule{\vx :^i \vS;\Gamma \vdash }{\vx :^i \vS;\Gamma \vdash \vx :^j\vS} i\le j\quad
\Rule{\vx \mapsto\vs:^i \vS;\Gamma \vdash }
         {\vx  \mapsto\vs:^i \vS;\Gamma \vdash \vx :^j\vS} i\le j

That is, higher level stuff can only be used for higher level things. We require of our design that the following be admissible

\Rule{\vdash \vt :^j \vT}{\vdash \vT:^{j+1}\Type}

So, contextuals and star (this stratification is orthogonal to stratification for consistency):

\Rule{\vdash \vS:^{i+1}\Type}{\vx:^i\vS\vdash}\quad
\Rule{\vdash \vs:^i\vS}{\vx\mapsto\vs:^i\vS\vdash}\quad

Next, the slight generalisation of ExTT to have a funny λ


\Rule{\vdash\vf:^j\forall\vx:^i\vS.\vT \quad \vdash\vs:^i\vS}

Plus the whatever conversion apparatus…

Next comes the deletion operator, ‘lightning’. The idea is just to erase types and everything which belongs at a higher level than the given index, leaving a ‘run-time’ λ-term.

$\Lightning$^j(\lambda\vx:^i\vS.\vt) & = & $\Lightning$^j\vt\quad\{\vi > \vj\} \\
                & = & \lambda\vx.$\Lightning$^j\vt\quad\{\vi \le \vj\} \\
$\Lightning$^j(\vf(\vs)^i) & = & $\Lightning$^j\vf \quad\{\vi > \vj\} \\
  & = & $\Lightning$^j\vf\:$\Lightning$^j\vs\quad\{\vi  \le \vj\} \\

$\Lightning$^j(!\vx\mapsto\vs:^i\vS.\vt) & = & $\Lightning$^j\vt\quad\{\vi > \vj\} \\
  & = & !\vx\mapsto$\Lightning$^j\vs.$\Lightning$^j\vt\quad\{\vi\le\vj\} \\
$\Lightning$^j\vx & = & \vx \\
$\Lightning^j(\forall\vx:^i\vS.\vT) & = & \bullet \\
$\Lightning$^j\Type & = & \bullet \\

Lightning extends to contexts in the obvious way, erasing the type annotations and the high-level entries. Any types which are present get replaced by a dummy token which can never be inspected. I claim

\(\)If \(i < j\) and \(\Gamma\vdash\vt:^i\vT\),
then \($\Lightning$^j\Gamma\vdash$\Lightning$^j\vt\)

where \vdash on untyped terms is the scoping judgment. The point is that variables whose bindings get erased only get used in places which also get erased. If lightning strikes the binding occurrence, it cannot strike any other occurrence.

Now, I claim that lightning commutes with reduction, in that, every reduction before erasure yields at most one reduction afterwards.

\(\)If \(i < j\), \(\Gamma\vdash\vt:^i\vT\) and \(\Gamma\vdash\vt\leadsto\vu\),
then \($\Lightning$^j\Gamma\vdash$\Lightning$^j\vt\leadsto^?$\Lightning$^j\vu\)

This is easily checked for β, δ, γ and structural rules.

We may now extend Edwin’s existing analysis of constructor and eliminator optimisation by making sure that all type-family arguments (eg motives) get quantified at a high level. Who says we can’t have an erasure semantics?

2 Responses to “Lightning”

  1. pwm Says:

    Now with real marvosym lightning. Don’t be too afraid

  2. Conor Says:


Leave a Reply