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

Dan Doel dan.doel at gmail.com
Thu Dec 2 20:25:41 CET 2010

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:

  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 

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 

Hope that helps some.

-- Dan

More information about the Haskell-Cafe mailing list