# Rendering of type-level computation

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.

• Are we doing "theory" here or are we actually thinking about how compilers work? Can you explain a bit what you're after? None of the rules you wrote would actually be used directly in a compiler. Aug 3, 2015 at 22:03
• @AndrejBauer Type theory is, to a substantial degree (although it has other uses), the theory of a specific compiler phase, namely semantic analysis. I used the term "compile-time computation" to emphasise that type-level computation is not normal computation. My use case is a lemma in a typing system that is be much easier to prove with the more general rule I was asking about. Aug 3, 2015 at 22:13
• Well, I wouldn't try to put your general rule in. Instead I would try to prove that it is admissible. Aug 3, 2015 at 23:33
• @AndrejBauer What goes wrong if I use it as a rule? Aug 4, 2015 at 7:23
• Probably nothing, since it looks admissible :-) Aug 4, 2015 at 10:19

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.

$$\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.

• Thanks. I know that the rule I gave didn't spell out all detail. I wanted to focus on the core of the issue. Why do we need the restriction to reduction rather than conversion? Aug 3, 2015 at 22:16
• Same reason: you can build ill-typed terms by naughty $\beta$-expansions.
– cody
Aug 4, 2015 at 12:48
• Should the top left $N$ in the first rule be $M$? Aug 5, 2015 at 17:22
• I simply understood @MartinBerger 's rule to implicitly require that $\alpha \equiv_{\mathrm{type}} \beta$ implies that $\alpha$ and $\beta$ are types. In general, I would always expect that we impose whatever conditions are necessary to avoid bringing in garbage. Aug 5, 2015 at 17:25
• @AndrejBauer: I agree completely. However, it's nice to know what a minimal set of such rules is (e.g. to make for simple implementations or avoid duplication of work) and sometimes interesting to see just how much garbage can actually come in. See for example kar.kent.ac.uk/21695/1/…
– cody
Aug 5, 2015 at 17:35