« Modules and Patching
Folding space »

Lightning

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):

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

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

\Rule{\vx:^i\vS\vdash\vT:^j\Type}{\vdash\forall\vx:^i\vS.\vT:^j\Type}\quad \Rule{\vx:^i\vS\vdash\vt:^j\vT}{\vdash\lambda\vx:^i\vS.\vt:^j\forall\vx:^i\vS.\vT}

\Rule{\vdash\vf:^j\forall\vx:^i\vS.\vT \quad \vdash\vs:^i\vS} {\vdash\vf(\vs)^i:^j!\vx\mapsto\vs:^i\vS.\vT}\quad \Rule{\vx\mapsto\vs:^i\vS\vdash\vt:^j\vT} {\vdash!\vx\mapsto\vs:^i\vS.\vt:^j!\vx\mapsto\vs:^i\vS.\vT}

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.

\begin{array}{lcl} $\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\} \\ \end{array}

\begin{array}{lcl} $\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 \\ \end{array}

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?

This entry was posted on Thursday, June 30th, 2005 at 11:15 am and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

2 Responses to “Lightning”

  1. pwm Says:
    July 5th, 2005 at 3:58 pm

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

  2. Conor Says:
    July 6th, 2005 at 2:15 pm

    Ta.

Leave a Reply