On 12/02/10 11:19, Iavor Diatchki wrote:
Hi, Bart Jacobs's book "Categorical Logic and Type Theory" has a categorical description of a system with dependent types (among others). The book is fairly advanced but it has lots of details about the constructions. Hope this helps, -Iavor
Page 586 of Jacobs' book mentions dependent products and dependent sums. What confuses me is that Nuprl defines the dependent product as a dependent function: http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionali... and the dependent sum as the dependent product: http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xpairs_doc.h... I sorta see that because the disjoint sum (i.e. the dependent product in Nuprl terms) is actually a pair of values, the discriminant (1st part) and the value whose type depends on the value of the discriminant. And I can see Nuprl's choice to call the dependent product as a dependent function because passing an index to this function returns a value whose type is dependent on the index. This is just like the value constructed by a haskell datatypes with field labels: data Record = MkRec { f1::T1, f2::T2, ..., fn::Tn } r = MkRec{ f1 = t1, f2 = t2,..., fn = tn} However, instead of r as the dependent function, the fields are the functions: fi r :: Ti, for i=1...n instead of Nuprl's notion: r fi :: Ti, for i=1...n Anybody know a good reason why the categorical and nuprl terms differ, leading, to (at least in my case) a bit of confusion? -Larry