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

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 [snip] *Maybe* the computer science people are trying to minimize the concepts. In this case, the one concept common to both the sum and product ( in

On 12/02/10 15:47, Iavor Diatchki wrote: the math peoples viewpoint) is there's a function: field2type: field_name -> Type in the case of a product or record, r, it's: product = f:fieldname -> field2type(f) in the case of a disjoint sum its: sum = (f:fieldname, field2type(f)) or something like that. -Larry

On 12/2/10 4:47 PM, Iavor Diatchki wrote:

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.

The product=function,sum=pair terminology comes from a certain interpretation of dependent types in set theory. I believe this originated with Per Martin-Löf's work, though I don't have any citations on hand. That terminology conflicts with the standard product=pair,sum=either terminology of functional languages, however. So folks from a functional background tend to prefer: dependent function, dependent product, sum; whereas folks from a set-theoretic background tend to prefer product, sum, <no name>/union. -- Live well, ~wren

Hi, thanks to all who gave me valuable pointers to what to study. It will take me some time to absorb that, but it helped a lot. Best regards, Petr On Thu, Dec 02, 2010 at 02:25:41PM -0500, Dan Doel wrote:

On Thursday 02 December 2010 10:13:32 am Petr Pudlak wrote:

...

Hi,

recently, I was studying how cartesian closed categories can be used to describe typed functional languages. Types are objects and morphisms are functions from one type to another.

Since I'm also interested in systems with dependent types, I wonder if there is a categorical description of such systems. The problem (as I see it) is that the codomain of a function depends on a value passed to the function.

I'd happy if someone could give me some pointers to some papers or other literature.

There are many different approaches to modelling dependent types in category theory. Roughly, they are all similar to modelling logic, but they all differ in details.

I think the easiest one to get a handle on is locally Cartesian closed categories, although there's some non-intuitive stuff if you're used to type theory. The way it works is this: a locally Cartesian closed category C is a category such that all its slice categories are cartesian closed. This gets you the following stuff:

---

Since C is isomorphic to C/1, where 1 is a terminal object, C is itself Cartesian closed assuming said 1 exists. This may be taken as a defining quality as well, I forget.

---

Each slice category C/A should be viewed as the category of A-indexed families of types. This seems kind of backwards at first, since the objects of C/A are pairs like (X, f : X -> A). However, the way of interpreting such f as a family of types F : A -> * is that F a corresponds to the 'inverse image' of f over a. So X is supposed to be like the disjoint union of the family F in question, and f identifies the index of any particular 'element' of X.

Why is this done? It has nicer theoretical properties. For instance, A -> * can't sensibly be a morphism, because * corresponds to the entire category of types we're modelling. It'd have to be an object of itself, but that's (likely) paradox-inducing.

---

Given a function f : B -> A, there's a functor f* : C/A -> C/B, which re- indexes the families. If you think of this in the more usual type theory style, it's just composition: B -f-> A -F-> *. In the category theoretic case, it's somewhat more complex, but I'll just leave it at that for now.

Now, this re-indexing functor is important. In type theories, it's usually expected to have two adjoints:

Σf ⊣ f* ⊣ Πf

These adjoints are the dependent sum and product. To get a base type that looks like:

Π x:A. B

from type theory. Here's how we go:

B should be A-indexed, so it's an object of C/A

For any A, there's an arrow to the terminal object ! : A -> 1

This induces the functor !* : C/1 -> C/A

This has an adjoint Π! : C/A -> C/1

C/1 is isomorphic to C, so C has an object that corresponds to Π!B, which is the product of the family B. This object is the type Π x:A. B

In general, ΠfX, with f : A -> B, and X an A-indexed family, F : A -> *, is the B-indexed family, G : B -> * for ease, where G b = Π x : f⁻¹ b. F x. That is, the product of the sub-family of X corresponding to each b. In the case of B = 1, this is the product of the entire family X.

This adjointness stuff is (no surprise) very similar to the way quantifiers are handled in categorical logic.

---

That's the 10,000 foot view. I wouldn't worry if you don't understand much of the above. It isn't easy material. In addition to locally Cartesian closed categories, you have:

toposes hyperdoctrines categories with families contextual categories fibred categories

And I'm probably forgetting several. If you read about all of these, you'll probably notice that there are a lot of similarities, but they mostly fail to be perfectly reducible to one another (although toposes are locally Cartesian closed).

I don't have any recommendations on a best introduction for learning this. Some that I've read are:

From Categories with Families to Locally Cartesian Closed Categories Locally Cartesian Closed Categories and Type Theory

but I can't say that any one paper made everything snap into place. More that reading quite a few gradually soaked in. And I still feel rather hazy on the subject.

Hope that helps some.

-- Dan