<p>In your reference [2], Barendregt shows that the rule</p>

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

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

<p>However there is an issue with your original rule already: the rule should read</p>

<p>$$ \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)$.</p>

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

<p>$$ \frac{\Gamma\vdash \alpha:s}{\Gamma,x:\alpha\ \ \mathrm{wf}}$$</p>

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

<p>This is a not completely trivial induction, using the following <strong>Lemma</strong>:</p>

<blockquote>
  <p>If $\Gamma\vdash t:\alpha$, $\Gamma\equiv\Delta$ and $\Delta\ \mathrm{wf}$ then $\Gamma\vdash t:\alpha$</p>
</blockquote>

<p>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.</p>

<hr>

<p>You could adopt the opposite point of view of keeping your more general conversion rule and <strong>weakening the context formation rule</strong> to</p>

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

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

CC BY-SA 3.0
2015-08-03T22:16:41.987Z
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?
Martin Berger
CC BY-SA 3.0
2015-08-04T12:48:42.913Z
Same reason: you can build ill-typed terms by naughty $\beta$-expansions.
cody
CC BY-SA 3.0
2015-08-05T17:22:42.193Z
Should the top left $N$ in the first rule be $M$?
Andrej Bauer
CC BY-SA 3.0
2015-08-05T17:25:46.957Z
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.
Andrej Bauer
CC BY-SA 3.0
2015-08-05T17:35:47.480Z
@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 https://kar.kent.ac.uk/21695/1/expansion_postponement_for_normalising_poll.pdf
cody
CC BY-SA 3.0
2015-08-05T19:33:42.407Z
@AndrejBauer  yes, I assume that $\alpha \equiv \beta$ means that $\alpha, \beta$ are types, but didn't want to clog the question with the details (which vary from system to system). And yes, it's nice to minimise the rules ... often makes proving things easier.
Martin Berger
CC BY-SA 3.0
2015-08-03T21:55:46.840Z
2015-08-03T21:55:46.840Z
cody
<p>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].</p>

<ul>
<li><p>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.</p></li>
<li><p>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
}
$$</p></li>
</ul>

<p>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</p>

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

<p>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?</p>

<hr>

<ol>
<li><p>H. Barendregt, <a href="http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf" rel="nofollow">Introduction to generalised type systems</a>.</p></li>
<li><p>H. Barendregt, <a href="http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf" rel="nofollow">Lambda Calculi with Types</a>.</p></li>
<li><p>B. C. Pierce, Types and Programming Languages.</p></li>
</ol>

CC BY-SA 3.0
2015-08-03T22:03:41.743Z
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.
Andrej Bauer
CC BY-SA 3.0
2015-08-03T22:13:03.020Z
@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.
Martin Berger
CC BY-SA 3.0
2015-08-03T23:33:36.220Z
Well, I wouldn't try to put your general rule in. Instead I would try to prove that it is admissible.
Andrej Bauer
CC BY-SA 3.0
2015-08-04T07:23:18.780Z
@AndrejBauer What goes wrong if I use it as a rule?
Martin Berger
CC BY-SA 3.0
2015-08-04T10:19:25.847Z
Probably nothing, since it looks admissible :-)
Andrej Bauer
CC BY-SA 3.0
2015-08-04T10:21:05.180Z
Now that I look at it more closely, you need to have $M \equiv_{\mathrm{Type}} N$ in a context. But which context, $\Gamma$ or $\Delta$? Same goes for $\alpha \equiv \beta$. That might be the reason for aversion to the rule: it forces you to break symmetry in an arbitrary fashion.
Andrej Bauer
CC BY-SA 3.0
2015-08-05T09:37:36.780Z
@AndrejBauer One way of preserving symmetry would be to have a two-sided type-equality, like so $\Gamma \vdash \alpha \equiv_{type} \beta \dashv \Delta$ where $\Gamma$ controls well-formedness of $\alpha$ and $\Delta$ does the same job for $\beta$.
Martin Berger
CC BY-SA 3.0
2015-08-05T17:21:57.620Z
Interesting, but would this work for arbitrary $\Gamma$ and $\Delta$? Can we write down reasonable rules for $\equiv_{\mathrm{type}}$ with such double sided contexts? (Transitivity looks tricky as it would bring in *three* contexts.) Isn't there some sort of a chat system around here?
Andrej Bauer
CC BY-SA 3.0
2015-08-05T19:51:08.010Z
@AndrejBauer I guess one needs to require that $\Gamma$ and $\Delta$ don't contradict each other, i.e. agree on the intersections of their respective domains. As to transitivity, the middle context that is cut out should be the same in both premises. What's a good (i.e. simple) calculus where one could try this out?
Martin Berger
<type-theory><type-systems><dependent-type><typed-lambda-calculus>
Rendering of type-level computation
Martin Berger
# Rendering of type-level computation

(Asked by: username_0 on 2015-08-03)

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](http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf).
2. H. Barendregt, [Lambda Calculi with Types](http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf).
3. B. C. Pierce, Types and Programming Languages.

**Tags:** type-theory, type-systems, dependent-type, typed-lambda-calculus
> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  
> **username_1**: Well, I wouldn't try to put your general rule in. Instead I would try to prove that it is admissible.  
> **username_0**: @AndrejBauer What goes wrong if I use it as a rule?  
> **username_1**: Probably nothing, since it looks admissible :-)  
> **username_1**: Now that I look at it more closely, you need to have $M \equiv_{\mathrm{Type}} N$ in a context. But which context, $\Gamma$ or $\Delta$? Same goes for $\alpha \equiv \beta$. That might be the reason for aversion to the rule: it forces you to break symmetry in an arbitrary fashion.  
> **username_0**: @AndrejBauer One way of preserving symmetry would be to have a two-sided type-equality, like so $\Gamma \vdash \alpha \equiv_{type} \beta \dashv \Delta$ where $\Gamma$ controls well-formedness of $\alpha$ and $\Delta$ does the same job for $\beta$.  
> **username_1**: Interesting, but would this work for arbitrary $\Gamma$ and $\Delta$? Can we write down reasonable rules for $\equiv_{\mathrm{type}}$ with such double sided contexts? (Transitivity looks tricky as it would bring in *three* contexts.) Isn't there some sort of a chat system around here?  
> **username_0**: @AndrejBauer I guess one needs to require that $\Gamma$ and $\Delta$ don't contradict each other, i.e. agree on the intersections of their respective domains. As to transitivity, the middle context that is cut out should be the same in both premises. What's a good (i.e. simple) calculus where one could try this out?  

---

## 1 answers

### Answer by username_2 on 2015-08-03. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: Same reason: you can build ill-typed terms by naughty $\beta$-expansions.  
> **username_1**: Should the top left $N$ in the first rule be $M$?  
> **username_1**: 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.  
> **username_2**: @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 https://kar.kent.ac.uk/21695/1/expansion_postponement_for_normalising_poll.pdf  
> **username_0**: @AndrejBauer  yes, I assume that $\alpha \equiv \beta$ means that $\alpha, \beta$ are types, but didn't want to clog the question with the details (which vary from system to system). And yes, it's nice to minimise the rules ... often makes proving things easier.  

---

