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

[Petr Pudlak]

Hi,

thanks to all who gave me valuable pointers to what to study. It will 
take me some time to absorb that, but it helped a lot.

     Best regards,
     Petr

On Thu, Dec 02, 2010 at 02:25:41PM -0500, Dan Doel wrote:
>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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20101207/bbde1030/attachment.pgp>