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.

  • $\begingroup$ 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. $\endgroup$ Aug 3 '15 at 22:03
  • $\begingroup$ @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. $\endgroup$ Aug 3 '15 at 22:13
  • $\begingroup$ Well, I wouldn't try to put your general rule in. Instead I would try to prove that it is admissible. $\endgroup$ Aug 3 '15 at 23:33
  • $\begingroup$ @AndrejBauer What goes wrong if I use it as a rule? $\endgroup$ Aug 4 '15 at 7:23
  • $\begingroup$ Probably nothing, since it looks admissible :-) $\endgroup$ Aug 4 '15 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.

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.

  • 1
    $\begingroup$ 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? $\endgroup$ Aug 3 '15 at 22:16
  • 1
    $\begingroup$ Same reason: you can build ill-typed terms by naughty $\beta$-expansions. $\endgroup$
    – cody
    Aug 4 '15 at 12:48
  • $\begingroup$ Should the top left $N$ in the first rule be $M$? $\endgroup$ Aug 5 '15 at 17:22
  • 1
    $\begingroup$ 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. $\endgroup$ Aug 5 '15 at 17:25
  • 1
    $\begingroup$ @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/… $\endgroup$
    – cody
    Aug 5 '15 at 17:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.