# Has a Dependent Type always a Type?

I am experimenting with dependent types. Lets assume the following short notation:

(πx:A.B)      The product type
(A -> B)      The product type when x does not occur in B


Now according to the generalized type system a triple (s1,s2,s3) regulates the formation of product types. We have the following formation rule:

G |- A : s1   D, x : A |- B : s2
-------------------------------- p-rule
G, D |- (πx:A.B) : s3


In the examples I have seen, the sorts are always atomic. Would it be possible to have a dependent sorts s2?

The question came up, when I tried to model the formation rule as a dependent type itself. My idea was that (πx:A.B) is a shorthand for a lambda expression where p is some predefined constant:

  πx:A.B   = p A (λx:A.B)


The following p's work:

1) p of type (πy:o.((y -> o) -> o))

it does the same as the triple (o,o,o), and thus says that if a is a proposition and b is a proposition, then a -> b is also a proposition (implication). This is how it works:

 |- p : (πy:o.((y -> o) -> o))  |- a : o       a : o |- a : o
---------------------------------------       --------------------
|- (p a) : ((a -> o) -> o)                    |- (a -> a) : a -> o
------------------------------------------------------------------
|- (p a (a -> a)) : o


1) p of type (πy:i.((y -> o) -> o))

it does the same as the triple (i,o,o), and thus says that if x from some set A and B(x) is a proposition, then (πx:A.B(x)) is a proposition (forall quantifier). This is how it works, assuming q : nat -> o:

 |- p : (πy:i.((y -> o) -> o))  |- nat : i     x : nat |- (q x) : o
-----------------------------------------     ---------------------------
|- (p nat) : ((nat -> o) -> o)                |- (λx:nat.(q x)) : nat -> o
-------------------------------------------------------------------------
|- (p nat (λx:nat.(q x))) : o


But I don't see how it should work when s2 is dependent. That s2 is dependent would mean that we have:

 D, x : A |- B : s2(x)


Have some logical systems where s2 is dependent already been studied? What would be the formation rule?

I guess we cannot go along with p : (πy:s1.((y-> s2(x)) -> s3)) because x has not the right scope.

Any ideas?

Bye

(*) H.P. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, 1(2):125-154, April 1991.

-
Pure type systems allow sorts to have structure and depend on types or values. In fact they completely eradicate the formal distinction between terms, types and sorts. On the other hand, all kinds of nice decidability properties tend to go down the drain when we reach that level of generality. – Henning Makholm Dec 27 '11 at 23:56
Thanks for the link, I didn't know about this terminological distinction. Do pure type systems work with a modified p-rule? Can we find a p for this p-rule? – j4n bur53 Dec 27 '11 at 23:59

There are dependent type systems where sorts can be dependent. One such example is advanced signature calculi for module type systems. Benjamin Pierce's Advanced Topics in Types and Programming Languages, §8.7 presents an example and references papers on the topic. In a nutshell, ML's type system is a polymorphic extension of simple types for the base language, but a dependent type system for the module language. An ML functor is a lambda expression with a dependent type:

$$\dfrac{\Gamma, A : S \vdash B : T} {\Gamma \vdash (\Lambda A:S. B) : (\Pi A:S. T)}$$

(Everything here is dependent, i.e. $A$ may occur in both $B$ and $T$. These are both module typing judgements: $A$ and $B$ are modules, $S$ and $T$ are signatures.) Many ML implementations allow modules to define names for signatures, with limited expressivity. There are proposals for signature calculi, where some computation is possible on signatures. Such calculi have (or at least admit) rules like

$$\dfrac{\Gamma \vdash A : S \qquad \Gamma \vdash S \equiv T} {\Gamma \vdash A : T}$$

i.e. if $S$ and $T$ are computationally equivalent signatures then any module that has the signature $A$ also has the signature $T$. Now if you introduce complex signatures, you need well-formedness judgements for signatures. Simple calculi can get away with $\Gamma \vdash S \;\mathtt{ok}$ (i.e. $S$ is well-formed), but more complex calculi need to express properties of fields of signatures, e.g. “the signatures $S$ and $T$ specify their field x in the same way”. This requires a dependent kinding system on signatures.

$$\dfrac{\Gamma \vdash T : K} {\Gamma \vdash \mathtt{sig}\; \mathtt{x} : T \;\mathtt{end} : \mathtt{SIG}(\mathtt{x} : T)}$$

Intuitively, read $\mathtt{SIG}(\mathtt{x} : T)$ as “a signature where the field x is specified as having the signature $T$”. I'm not going to give a full definition of such a calculus here. For an example (with different notations), see ATTAPL or “An Expressive Language of Signatures” by Ramsey, Fisher and Govereau.

There's a different approach, which consists of erasing the level distinction: instead of having a hierarchy of terms, types and sorts, treat everything as a term, and possibly allow an infinite hierarchy where $\vdash t_0 : t_1$, $\vdash t_1 : t_2$, etc. A seminal example is the calculus of constructions. There, the rules for the formation of product types and products are

$$\begin{gather*} \dfrac{\Gamma, x:A \vdash B : S \qquad \text{S is a sort}} {\Gamma \vdash (\forall x:A. B) : S} \ \dfrac{\Gamma, x:A \vdash t : B} {\Gamma \vdash (\lambda x:A. t) : (\forall x:A. B)} \ \end{gather*}$$

I'll refer you to a formal presentation for what “$S$ is a sort means”; roughly speaking, a sort is the type of a term which is itself the type of another term. Note that in the calculus of constructions, sorts are not dependent (in that $S$ here does not contain $x$); however, because of the lack of a level constraint, a lambda expression can operate and return types, sorts, sorts of sorts, etc.

The best way to learn the calculus of constructions is to play with it in the Coq interactive theorem prover. Its reference manual contains a definition of most of the underlying calculus (see the referenced papers for some of the details, mainly the precise rules for well-founded recursions).

-
@CookieMonster The reason I included CoC is that there is no stratification, in the sense that an object which is $s_3$ in one typing judgement can be $s_1$ in another judgement. It's a generalization in a different direction from syntactically dependent sorts, but it does result in semantically dependent sorts. – Gilles Jan 9 '12 at 2:34

I guess the following type would solve the problem:

p of type (py:s1.((px:y.s2(x)) -> s3)

Lets check it, assuming:

G |- A : s1


and:

D, x : A |- B : s2(x)


We should arrive at:

G, D |- (p A (lx:A.B)) : s3


Here is a derivation that exactly does this:

|- p : (py:s1.((px:y.s2(x)) -> s3)   G |- A : s1    D, x : A |- B : s2(x)
------------------------------------------------    ----------------------------
G |- (p A) : ((px:A.s2(x)) -> s3)                   D |- (lx:A.B) : (px:A.s2(x))
--------------------------------------------------------------------------------
G, D |- (p A (lx:A.B)) : s3


General problem with asking this kind of question: The product type itself is used in the type of p. So cannot be used to fully eliminate product types.

But at least it reduces the type judgement for product types to the type judgement of a constant, a lambda abstract and two applications.

Could eventually lead to a different representation of tripples (s1,s2,s3)...

Bye

-