Rendering of type-level computation

Question

Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some details for simplicity), see e.g. [1, 2, 3].

• A notion $\equiv_{type}$ of type-equivalence is defined on types, e.g. $(\lambda x^{K}.\alpha)\beta \equiv_{type} \alpha[\beta/x]$ or $(\Pi x^{\alpha}.\beta)M \equiv_{type} \beta[M/x]$, where $M$ ranges over programs, $K$ over kinds, and $\alpha, \beta$ over types.

• Then the typing system is enriched with a variant of the following rule. $$ \frac{ \Gamma \vdash M : \alpha \quad \alpha \equiv_{type} \beta }{ \Gamma \vdash M : \beta } $$

However, we can easily extend the relation $\equiv_{type}$ to typing environments $\Gamma$ pointwise, and also to programs, e.g. $\lambda x^{\alpha}.M \equiv_{type} \lambda x^{\beta}.M$ whenever $\alpha \equiv_{type} \beta$, leading to a rule

$$ \frac{ \Gamma \vdash M : \alpha \quad \Gamma \equiv_{type} \Delta \quad M \equiv_{type} N \quad \alpha \equiv_{type} \beta }{ \Delta \vdash N : \beta } $$

I have never seen this done. I assume that it's just a question of convenience and that both approaches are equally expressive, but I am not sure! Is there some problem with the second approach?

---

1. H. Barendregt, Introduction to generalised type systems.

2. H. Barendregt, Lambda Calculi with Types.

3. B. C. Pierce, Types and Programming Languages.

Answer 1

In your reference [2], Barendregt shows that the rule

$$ \frac{\Gamma\vdash N:\alpha\quad M\rightarrow^* N\quad \alpha\equiv \beta}{\Gamma\vdash N:\beta} $$

is indeed admissible for Pure Type Systems, as (a trivial consequence of) Corollary 5.2.16.

However there is an issue with your original rule already: the rule should read

$$ \frac{\Gamma\vdash N:\alpha\quad\alpha\equiv \beta\quad {\bf \Gamma\vdash\beta : s}}{\Gamma\vdash N:\beta} $$ for some sort $s$, otherwise you may introduce ill-formed types into your typing judgement, like $(\lambda x y. y)\ \Omega\ (\alpha\rightarrow\alpha)$.

This can be a problem for your extended rule, as usually you only allow well-formed types into your context, with a rule along the lines of

$$ \frac{\Gamma\vdash \alpha:s}{\Gamma,x:\alpha\ \ \mathrm{wf}}$$

If you add the relevant well-formedness requirements ($\Delta\ \mathrm{wf}$ and $\Delta\vdash\beta:s$), and restrict the term level to reduction rather than conversion, then your sophisticated rule becomes admissible.

This is a not completely trivial induction, using the following Lemma:

If $\Gamma\vdash t:\alpha$, $\Gamma\equiv\Delta$ and $\Delta\ \mathrm{wf}$ then $\Gamma\vdash t:\alpha$

The lemma is proven by induction using an application of the conversion rule at the variable case. The theorem is then proven using the above lemma to discharge the conversion case.

---

You could adopt the opposite point of view of keeping your more general conversion rule and weakening the context formation rule to

$$ \frac{\Gamma\vdash \beta:s\quad \beta\equiv \alpha}{\Gamma,x:\alpha\ \ \mathrm{wf}}$$

then you get a system with possibly ill-formed types, but no additional typeable terms, though I think this is a very non-trivial result.