[Haskell-cafe] Categorical description of systems with dependent types
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:
> 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
There are many different approaches to modelling dependent types in category
theory. Roughly, they are all similar to modelling logic, but they all differ
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
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
Π 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
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.
More information about the Haskell-Cafe