3
$\begingroup$

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.

  • 0
    [Pure type systems](http://en.wikipedia.org/wiki/Pure_type_system) 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.2011-12-27
  • 0
    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?2011-12-27

2 Answers 2