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