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

[Dan Doel]

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