<p>Part of the problem is we <em>cannot</em> say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ reduces to a hypothetico-general judgment.</p>

<p>In practice, the way that you implement this kind of type theory is by formalizing rules for hypothetico-general equality &amp; membership as a kind of sequent calculus, and then you can write tactics that automate as much of the work as possible. This is the technique used in Nuprl, JonPRL and RedPRL, which all implement type theories of the kind that you describe in your post.</p>

CC BY-SA 3.0
2017-02-04T23:39:33.197Z
2017-02-04T23:39:33.197Z
Jonathan Sterling
<p>We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). Now according to Martin-Löf's meaning explanations [1], a hypothetical judgment of the form
$$ x_1 : A_1, ..., x_n : A_n \vdash a : A \qquad\qquad\qquad\qquad\qquad\qquad (1)$$
means that
$$ \vdash a[x_1,...,x_n/a_1,...,a_n] : [x_1,...,x_n/a_1,...,a_n]A \qquad (2)$$
for all closed terms $a_1 : A_1, ..., a_n : A_n$ (and also that this judgment should be functional in respect to judgmental equality, but I don't need to tackle this issue here).</p>

<p>This means, among other things, that the judgment
$$ x : \mathsf{empty} \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat}  \qquad\qquad\qquad\qquad\qquad\qquad\quad (3)$$
is derivable in the theory, since there are no closed terms of the empty type (for the condition given is vacuously true). But also that less obvious judgments are also vacuously evident:
$$ x : \mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty}) \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad (4)$$
since any closed term of $\mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty})$ gives us a closed term of $\mathsf{empty}$, which should have none.</p>

<p>My question is:</p>

<blockquote>
  <p>What is a nice way to implement a type checker for such a hypothetical judgments?</p>
</blockquote>

<p>(I'm aware that the problem is undecidable in general, but in theory this should affect us only in the sense that we are unable to rule out all invalid judgments).</p>

<p>For simplicity, we can suppose that we already have a type checking algorithm for categorical judgments.</p>

<p>IMHO$-$and in the spirit of the universal introduction rule of predicate logic$-$the obvious type checking algorithm for (1) to say that it is valid whenever $$\vdash a[x_1,...,x_n/t_1,...,t_n] : [x_1,...,x_n/t_1,...,t_n]A$$ for a list of <em>arbitraries</em> closed terms $t_1 : A_1 ,..., t_n : A_n $ (since we can't possibly consider each closed term of such types). However, this algorithm is clearly unable to validate sequents such as (3), let alone (4). </p>

<p>There is a quick highly-inelegant fix, which is to add the condition that if you find $x : \mathsf{empty}$ in the context list, halt and automatically recognize the whole sequent as true. But what about not-so-evident vacuously evident judgments such as (4)?</p>

<p>Anyway, how would a correct, elegant and general approach look like?</p>

<p>PS: I'm sorry if the question is not precise enough, but I can't think of a better way to state it.</p>

<p>[1] Martin-Löf, Constructive Mathematics and Computer Programming, 1982.</p>

CC BY-SA 3.0
2016-10-09T19:23:49.343Z
I don't get your motivating example: are you saying that there are no inhabitants of $A\times (A \rightarrow \mathrm{empty})$? That really depends on $A$.
cody
CC BY-SA 3.0
2016-10-10T02:49:01.167Z
@cody I made an edit with a concrete instance of $A$ to make my point clearer.
StudentType
CC BY-SA 3.0
2016-10-10T07:17:33.967Z
Are you looking for [Andromeda](http://andromedans.github.io/andromeda/index.html)? It can derive these crazy things. Of course, not completely by itself, but with a bit of hints.
Andrej Bauer
CC BY-SA 3.0
2016-10-13T11:36:25.223Z
I think you're looking for the equality reflection rule -- prove it sound with respect to your realizability semantics, and then prove (4) by proving that → is propositionally equal to  in the inconsistent context, and so they are definitionally equal, and so you get (4) from the obvious 1 : nat.
Neel Krishnaswami
<type-theory><type-systems><dependent-type><typed-lambda-calculus>
Type checking, Hypothetical judgments, meaning explanations and computational type theory
StudentType
# Type checking, Hypothetical judgments, meaning explanations and computational type theory

(Asked by: username_0 on 2016-10-09)

We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). Now according to Martin-Löf's meaning explanations [1], a hypothetical judgment of the form
$$ x\_1 : A\_1, ..., x\_n : A\_n \vdash a : A \qquad\qquad\qquad\qquad\qquad\qquad (1)$$
means that
$$ \vdash a[x\_1,...,x\_n/a\_1,...,a\_n] : [x\_1,...,x\_n/a\_1,...,a\_n]A \qquad (2)$$
for all closed terms $a\_1 : A\_1, ..., a\_n : A\_n$ (and also that this judgment should be functional in respect to judgmental equality, but I don't need to tackle this issue here).

This means, among other things, that the judgment
$$ x : \mathsf{empty} \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad\qquad\qquad\quad (3)$$
is derivable in the theory, since there are no closed terms of the empty type (for the condition given is vacuously true). But also that less obvious judgments are also vacuously evident:
$$ x : \mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty}) \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad (4)$$
since any closed term of $\mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty})$ gives us a closed term of $\mathsf{empty}$, which should have none.

My question is:

> What is a nice way to implement a type checker for such a hypothetical judgments?

(I'm aware that the problem is undecidable in general, but in theory this should affect us only in the sense that we are unable to rule out all invalid judgments).

For simplicity, we can suppose that we already have a type checking algorithm for categorical judgments.

IMHO$-$and in the spirit of the universal introduction rule of predicate logic$-$the obvious type checking algorithm for (1) to say that it is valid whenever $$\vdash a[x\_1,...,x\_n/t\_1,...,t\_n] : [x\_1,...,x\_n/t\_1,...,t\_n]A$$ for a list of *arbitraries* closed terms $t\_1 : A\_1 ,..., t\_n : A\_n $ (since we can't possibly consider each closed term of such types). However, this algorithm is clearly unable to validate sequents such as (3), let alone (4).

There is a quick highly-inelegant fix, which is to add the condition that if you find $x : \mathsf{empty}$ in the context list, halt and automatically recognize the whole sequent as true. But what about not-so-evident vacuously evident judgments such as (4)?

Anyway, how would a correct, elegant and general approach look like?

PS: I'm sorry if the question is not precise enough, but I can't think of a better way to state it.

[1] Martin-Löf, Constructive Mathematics and Computer Programming, 1982.

**Tags:** type-theory, type-systems, dependent-type, typed-lambda-calculus
> **Comments:**
> **username_1**: I don't get your motivating example: are you saying that there are no inhabitants of $A\times (A \rightarrow \mathrm{empty})$? That really depends on $A$.  
> **username_0**: @cody I made an edit with a concrete instance of $A$ to make my point clearer.  
> **username_2**: Are you looking for [Andromeda](http://andromedans.github.io/andromeda/index.html)? It can derive these crazy things. Of course, not completely by itself, but with a bit of hints.  
> **username_3**: I think you're looking for the equality reflection rule -- prove it sound with respect to your realizability semantics, and then prove (4) by proving that → is propositionally equal to  in the inconsistent context, and so they are definitionally equal, and so you get (4) from the obvious 1 : nat.  

---

## 1 answers

### Answer by username_4 on 2017-02-04. Score: 6

Part of the problem is we *cannot* say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ reduces to a hypothetico-general judgment.

In practice, the way that you implement this kind of type theory is by formalizing rules for hypothetico-general equality & membership as a kind of sequent calculus, and then you can write tactics that automate as much of the work as possible. This is the technique used in Nuprl, JonPRL and RedPRL, which all implement type theories of the kind that you describe in your post.


---

