Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

(px: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 |- (px: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 (px:A.B) is a shorthand for a lambda expression where p is some predefined constant:

  px:A.B   = p A (lx:A.B)

The following p's work:

1) p of type (py: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 : (py: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 (py: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 (px:A.B(x)) is a proposition (forall quantifier). This is how it works, assuming q : nat -> o:

 |- p : (py:i.((y -> o) -> o))  |- nat : i     x : nat |- (q x) : o
 -----------------------------------------     ---------------------------
 |- (p nat) : ((nat -> o) -> o)                |- (lx:nat.(q x)) : nat -> o
 -------------------------------------------------------------------------
                       |- (p nat (lx: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 : (py: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.

share|improve this question
    
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
    
Just reading: Jan-Willem Roorda, Pure Type Systems for Functional Programming, is (PI) rule would not work when x in t. –  j4n bur53 Dec 28 '11 at 0:12

2 Answers 2

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

share|improve this answer

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

share|improve this answer
    
@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
    
Calculus of construction as you show it is an instance of a generalized type system where (s1,s2,s3) = (_,S,S). But you also write S does not contain x, so we do not have the dependence here that I would be interested in. –  j4n bur53 Jan 9 '12 at 2:39
    
The SIG rule looks to me like a lambda-rule à la Barendregt and not like a p-rule à la Barendregt. Similar to the last rule you show for the calculus of construction and the first rule you show for ML. In the full formulation à la Barendregt some additional judgements are necessary, but it is seen that even if there were some dependency on s2, since the s2 drops out in the conclusion, there is no problem with scope in a lambda-rule (page 136). The problem is only there for p-rules. –  j4n bur53 Jan 9 '12 at 2:43
    
The rules for sort judgements in calculus of construction are Prop:Type(0), Set:Type(0) and Type(i):Type(i+1), and i is infered. How do you get a dependency of the quality of D, x : A |- B : s2(x) from this? Either semantically or syntactically? Is convertibility needed? –  j4n bur53 Jan 9 '12 at 3:41

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.