[Haskell-cafe] Categorical description of systems with dependent types

[Larry Evans]

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/Xfunctionality2_doc.html

and the dependent sum as the dependent product:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xpairs_doc.html

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