[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:
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
More information about the Haskell-Cafe
mailing list