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

[Iavor Diatchki]

Hi,
You have it exactly right, and I don't think that there's a
particularly deep reason to prefer the one over the other.  It seems
that computer science people
tend to go with the (product-function) terminology, while math people
seem to prefer the (sum-product) version, but it is all largely a
matter of taste.
-Iavor


On Thu, Dec 2, 2010 at 11:03 AM, Larry Evans <cppljevans at suddenlink.net> wrote:
> 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
>
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>