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.