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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe