1
$\begingroup$

In type theory, we usually define each type with a constant symbol, e.g., the dependent product uses '$\Pi$', the dependent sum uses '$\Sigma$', the sum/coproduct uses '$+$'. I noticed that we could possibly reformulate these symbols as terms within the language itself. To demonstrate, we introduce a constant term '$\Pi$' such that given any type $A$ and any function $B$ from $A$ to types, $\Pi\ A\ B$ is also a type. Formally, let $x$ be a variable and $A$ and $B$ be terms; $$\begin{array}{c} A:\mathsf{Type}\quad x:A\vdash B\ x:\mathsf{Type} \\ \hline \Pi\ A\ B:\mathsf{Type} \end{array}$$ where $x$ does not occur free in $A$ nor $B$. Other types can be constructed similarly. For my question, is there any interesting consequences/benefits to formulizing a type theory this way, or is there any good reason it should not be done like this?

I thought it might be interesting since under this formulation, we can manipulate the $\Pi$ term itself, as well as abstract over its second argument, e.g., $$\lambda A:\mathsf{Type}\ .\lambda B:(\Pi\ A\ x:A\ .\mathsf{Type})\ .\Pi\ A\ B,$$ all of which I haven't seen done in traditional type theory. Additionally, $\Pi$ is typable: $$\Pi:\Pi\ \mathsf{Type}\ A:\mathsf{Type}\ .\Pi\ (\Pi\ A\ x:A\ .\mathsf{Type})\ B:(\Pi\ A\ x:A\ .\mathsf{Type})\ .\mathsf{Type}.$$

$\endgroup$
3
  • $\begingroup$ this doesn't quite work - you write $\Pi A \;B : Type$ when you really need to write $\Pi x:A, B : Type$. The fact that $x$ must occur in the definition of the $\Pi$ type in question seems to defeat your goal of making $\Pi$ a term. $\endgroup$ Aug 2, 2021 at 1:56
  • $\begingroup$ @MarkSaving $B$ is a function type from $A$ to $\mathsf{Type}$, so we do not need to specify a variable. If $f:\Pi\ A\ B$ and $x:A$, then $f\ x:B\ x$ where $B\ x$ is just function application and $B\ x:\mathsf{Type}$. $\endgroup$
    – Kainoa B
    Aug 2, 2021 at 2:19
  • $\begingroup$ Ah, I see. I believe I have come up with a satisfactory answer to your question; see below. $\endgroup$ Aug 2, 2021 at 3:44

2 Answers 2

2
$\begingroup$

The issue here is in the very definition of the $\Pi$ type. The only type which must be a primitive is the $\Pi$ type - the rules for other types can be defined in terms of the rules for $\Pi$.

I will assume you're using infinite universes. Rather than $\mathsf{Type}$, I will write $\mathsf{Type}_i$ for the $i$th level of types.

Consider the judgement $A : \mathsf{Type}_0 \vdash \lambda x : A . \mathsf{Type}_j : \Pi A (\lambda x : A . \mathsf{Type}_{j + 1})$. I claim that this judgement can never be made.

For if we were to make this judgement using your rule, we would first need the judgement $A : \mathsf{Type}_0, x : A \vdash (\lambda x . \mathsf{Type}_j) x : \mathsf{Type}_{j + 1}$. And in order to come to this conclusion, we would need to apply the elimination rule, which states that

$$\begin{array}{c} A:\mathsf{Type_i}\quad x:A\vdash B\ x:\mathsf{Type_i} \quad f : \Pi A \;B \quad a : A\\ \hline f a : B[x \mapsto a] \end{array}$$

where $B[x \mapsto a]$ is the obvious capture-avoiding substitution. But in order to apply this rule (in the context $A : \mathsf{Type}_i$), we would need the conclusion that $A : \mathsf{Type} \vdash \lambda x . \mathsf{Type}_j : \Pi A (\lambda x . \mathsf{Type}_{j + 1})$.

But this is the very judgement we seek to derive. So in order to come up with a derivation of the judgement, we would need to have already derived the judgement. So clearly, the judgement can never be made.

Now clearly, it is possible to work around this if you're willing to dramatically alter the entire landscape of rules. For example, you could add a second, special elimination rule specifically for giving a type to terms of the form $(\lambda x : A . T) y$. But this ruins the harmonious structure of type checking in which there is only a single rule which can ever be the last one used in a typing judgement $x : Z$, since there will be two different elimination rules which can both cover the judgement $(\lambda x : A . T)y$.

$\endgroup$
3
  • $\begingroup$ I'm not sure where you get $A:\mathsf{Type}_0, x:A\vdash(\lambda x\ .\mathsf{Type}_j)\ x:\mathsf{Type}_{j+1}$. If we're using the introduction rule $$\begin{array}{c}x:A\vdash t:B\ x\\ \hline \lambda x:A\ .t:\Pi\ A\ B\end{array}$$ (omitting the type verifications), shouldn't we get $A:\mathsf{Type}_0, x:A\vdash\mathsf{Type}_j:(\lambda x:A\ .\mathsf{Type}_{j+1})\ x$ instead? In either case, doesn't the above immediately follow from $A:\mathsf{Type}_0, x:A\vdash\mathsf{Type}_j:\mathsf{Type}_{j+1}$ by the computation rule, i.e., $\beta$-reduction? This seems to bypass the elimination rule. $\endgroup$
    – Kainoa B
    Aug 2, 2021 at 6:51
  • $\begingroup$ @KainoaB The $\beta$-rule only gives you $(\lambda x : A . \mathsf{Type}_j) x \equiv_{\mathsf{Type}_{j + 1}} \mathsf{Type}_j$. However, it is actually a meta-theorem (an admissible rule) that if $T_1 \equiv_{T_2} T_3$ then $T_1 : T_2$, not a rule in itself. The rule does not hold in your system (or, to be precise, it is not an admissible rule). $\endgroup$ Aug 2, 2021 at 15:15
  • $\begingroup$ In addition, sometimes people introduce a "logical framework", which is a sort of meta-theory with its own $\Pi$-types. This enables a non-circular expression of the $\Pi$-types (and other types) of the object theory in terms of the $\Pi$-types and universe of the meta-theory. $\endgroup$ Aug 3, 2021 at 7:07
0
$\begingroup$

I want to rework the answer given by @MarkSaving since I believe he is correct but I do not think his reasoning matches the type rules I had in mind. Hence, I will give an alternative path to show that formalizing $\Pi$ as a term is inadequate. Just to be clear, let's give some of our type rules using $\Pi$ as a term: $$\cfrac{\Gamma\ ,\ x\ {:}\ \alpha\ {\vdash}\ B\ {:}\ \beta\ x}{\Gamma\ {\vdash}\ x\ {:}\ \alpha\ .\ B\ {:}\ \Pi\ \alpha\ \beta}\ \Pi\textit{-Intro}$$ $$\cfrac{\Gamma\ {\vdash}\ f\ {:}\ \Pi\ \alpha\ \beta\qquad\Gamma\ {\vdash}\ a\ {:}\ \alpha}{\Gamma\ {\vdash}\ f\ a\ {:}\ \beta\ a}\ \Pi\textit{-Elim}$$ We include an infinite cumulative hierarchy of universes: $\mathsf{Type}_0$, $\mathsf{Type}_1$, $\mathsf{Type}_2$, $\ldots$ $$\cfrac{\Gamma\ {\vdash}\ A\ {:}\ \alpha\qquad\Gamma\ {\vdash}\ \alpha'\ {:}\ \mathsf{Type}_i}{\Gamma\ {\vdash}\ A\ {:}\ \alpha'}\ \textit{Conv}\quad\text{if $\alpha=_\beta\alpha'$}$$ As claimed by @MarkSaving, we will also demonstrate that the following judgment is not derivable: \begin{equation} \alpha\ {:}\ \mathsf{Type}_0\ {\vdash}\ x\ {:}\ \alpha\ .\ \mathsf{Type}_i\ {:}\ \Pi\ \alpha\ (\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ ) \tag{1} \end{equation} To derive (1), we need to use $\Pi$-Intro, which requires us to derive \begin{equation} \alpha\ {:}\ \mathsf{Type}_0\ ,\ x\ {:}\ \alpha\ {\vdash}\ \mathsf{Type}_i\ {:}\ (\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ )\ x. \tag{2} \end{equation} Again, to derive (2), we need to use Conv (since $\mathsf{Type}_{i+1}=_\beta(\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ )\ x$), which requires us to derive \begin{equation} \alpha\ {:}\ \mathsf{Type}_0\ ,\ x\ {:}\ \alpha\ {\vdash}\ (\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ )\ x\ {:}\ \mathsf{Type}_{i+2}. \tag{3} \end{equation} Finally, to derive (3), we need to use $\Pi$-Elim, which requires us to derive \begin{equation} \alpha\ {:}\ \mathsf{Type}_0\ ,\ x\ {:}\ \alpha\ {\vdash}\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ {:}\ \Pi\ \alpha\ (\ z\ {:}\ \alpha\ .\ \mathsf{Type}_{i+2}\ ). \tag{4} \end{equation} Notice that the right hand sides (of the turnstiles) of (4) and (1) are essentially the same. Hence, the above reasoning can be applied infinitely, requiring us to derive \begin{equation} \alpha\ {:}\ \mathsf{Type}_0\ ,\ x_0\ {:}\ \alpha\ ,\ \ldots\ ,\ x_{n-2}\ {:}\ \alpha\ {\vdash}\ x_{n-1}\ {:}\ \alpha\ .\ \mathsf{Type}_j\ {:}\ \Pi\ \alpha\ (\ x_n\ {:}\ \alpha\ .\ \mathsf{Type}_{j+1}\ ) \tag{5} \end{equation} for higher and higher values of $j$ without terminating. Thus, by infinite descent, (1) is not derivable.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .