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.
 A: 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).
A: 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
