Re: [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


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[wren ng thornton]

On 12/2/10 4:47 PM, Iavor Diatchki wrote:

Hi,
You have it exactly right, and I don't think that there's a
particularly deep reason to prefer the one over the other.  It seems
that computer science people
tend to go with the (product-function) terminology, while math people
seem to prefer the (sum-product) version, but it is all largely a
matter of taste.


The product=function,sum=pair terminology comes from a certain 
interpretation of dependent types in set theory. I believe this 
originated with Per Martin-Löf's work, though I don't have any citations 
on hand.


That terminology conflicts with the standard product=pair,sum=either 
terminology of functional languages, however. So folks from a functional 
background tend to prefer: dependent function, dependent product, sum; 
whereas folks from a set-theoretic background tend to prefer product, 
sum, no name/union.


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Petr Pudlak]

 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.


Thanks,
Petr


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Larry Evans]

On 12/02/10 09:13, 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.
 
 Thanks,
 Petr

Hi Petr,

Although it's not a categorical description of dependent types (AFAICT,
but I've almost no experience in category theory), dependent types
are described by Nuprl:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html

For example, on that page, there's this:

  Actually, A-B is a special form of the more general x:A-C(x). When
  A is a type and C(x) is a type-valued function (in x) over domain A,
  then a member of x:A-C(x) is a function which for an argument, a:A
  takes a value in the type C(a).

HTH.

-Larry


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[roconnor]

On Thu, 2 Dec 2010, 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.


Voevodsky talks about the category of contexts in 
http://www.mefeedia.com/watch/31778282, which I understand is described 
in more detail in Semantics of type theory : correctness, completeness, 
and independence results by Thomas Streicher.


--
Russell O'Connor  http://r6.ca/
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Iavor Diatchki]

Hi,
Bart Jacobs's book Categorical Logic and Type Theory has a
categorical description of a system with dependent types (among
others).  The book is fairly advanced but it has lots of details about
the constructions.
Hope this helps,
-Iavor

On Thu, Dec 2, 2010 at 8:18 AM,  rocon...@theorem.ca wrote:
 On Thu, 2 Dec 2010, 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.

 Voevodsky talks about the category of contexts in
 http://www.mefeedia.com/watch/31778282, which I understand is described in
 more detail in Semantics of type theory : correctness, completeness, and
 independence results by Thomas Streicher.

 --
 Russell O'Connor                                      http://r6.ca/
 ``All talk about `theft,''' the general counsel of the American Graphophone
 Company wrote, ``is the merest claptrap, for there exists no property in
 ideas musical, literary or artistic, except as defined by statute.''

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Larry Evans]

On 12/02/10 11:19, Iavor Diatchki wrote:
 Hi,
 Bart Jacobs's book Categorical Logic and Type Theory has a
 categorical description of a system with dependent types (among
 others).  The book is fairly advanced but it has lots of details about
 the constructions.
 Hope this helps,
 -Iavor
 

Page 586 of Jacobs' book mentions dependent products and dependent sums.
What confuses me is that Nuprl defines the dependent product as
a dependent function:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html

and the dependent sum as the dependent product:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xpairs_doc.html

I sorta see that because the disjoint sum (i.e. the dependent product
in Nuprl terms) is actually a pair of values, the discriminant (1st
part) and the value whose type depends on the value of the discriminant.
And I can see Nuprl's choice to call the dependent product as a
dependent function because passing an index to this function returns
a value whose type is dependent on the index. This is just like
the value constructed by a haskell datatypes with field labels:

  data Record = MkRec { f1::T1, f2::T2, ..., fn::Tn }
  r = MkRec{ f1 = t1, f2 = t2,..., fn = tn}

However, instead of r as the dependent function, the fields are the
functions:

   fi r :: Ti,  for i=1...n

instead of Nuprl's notion:

   r fi :: Ti,  for i=1...n

Anybody know a good reason why the categorical and nuprl terms
differ, leading, to (at least in my case) a bit of confusion?


-Larry




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [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

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Iavor Diatchki]

Hi,
You have it exactly right, and I don't think that there's a
particularly deep reason to prefer the one over the other.  It seems
that computer science people
tend to go with the (product-function) terminology, while math people
seem to prefer the (sum-product) version, but it is all largely a
matter of taste.
-Iavor


On Thu, Dec 2, 2010 at 11:03 AM, Larry Evans cppljev...@suddenlink.net wrote:
 On 12/02/10 11:19, Iavor Diatchki wrote:
 Hi,
 Bart Jacobs's book Categorical Logic and Type Theory has a
 categorical description of a system with dependent types (among
 others).  The book is fairly advanced but it has lots of details about
 the constructions.
 Hope this helps,
 -Iavor


 Page 586 of Jacobs' book mentions dependent products and dependent sums.
 What confuses me is that Nuprl defines the dependent product as
 a dependent function:


 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html

 and the dependent sum as the dependent product:


 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xpairs_doc.html

 I sorta see that because the disjoint sum (i.e. the dependent product
 in Nuprl terms) is actually a pair of values, the discriminant (1st
 part) and the value whose type depends on the value of the discriminant.
 And I can see Nuprl's choice to call the dependent product as a
 dependent function because passing an index to this function returns
 a value whose type is dependent on the index. This is just like
 the value constructed by a haskell datatypes with field labels:

  data Record = MkRec { f1::T1, f2::T2, ..., fn::Tn }
  r = MkRec{ f1 = t1, f2 = t2,..., fn = tn}

 However, instead of r as the dependent function, the fields are the
 functions:

   fi r :: Ti,  for i=1...n

 instead of Nuprl's notion:

   r fi :: Ti,  for i=1...n

 Anybody know a good reason why the categorical and nuprl terms
 differ, leading, to (at least in my case) a bit of confusion?


 -Larry




 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Larry Evans]

On 12/02/10 15:47, Iavor Diatchki wrote:
 Hi,
 You have it exactly right, and I don't think that there's a
 particularly deep reason to prefer the one over the other.  It seems
 that computer science people
 tend to go with the (product-function) terminology, while math people
 seem to prefer the (sum-product) version, but it is all largely a
 matter of taste.
 -Iavor
[snip]
*Maybe* the computer science people are trying to minimize the concepts.
In this case, the one concept common to both the sum and product ( in
the math peoples viewpoint) is there's a function:

   field2type: field_name - Type

in the case of a product or record, r, it's:

  product = f:fieldname - field2type(f)

in the case of a disjoint sum its:

  sum = (f:fieldname, field2type(f))

or something like that.

-Larry


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Dan Doel]

On Thursday 02 December 2010 7:54:18 pm Larry Evans wrote:
 [snip]
 *Maybe* the computer science people are trying to minimize the concepts.
 In this case, the one concept common to both the sum and product ( in
 the math peoples viewpoint) is there's a function:
 
field2type: field_name - Type
 
 in the case of a product or record, r, it's:
 
   product = f:fieldname - field2type(f)
 
 in the case of a disjoint sum its:
 
   sum = (f:fieldname, field2type(f))
 
 or something like that.

I'll be honest: I don't really know what you're saying above. However, I can 
throw in my 2 cents on the naming thing.

The product-function naming obviously comes from thinking about, what if the 
type of later arguments of a tuple could depend on earlier ones, and what if 
the result type of a function could depend on the argument? These are quite 
ordinary questions for a practicing programmer to think about, which is 
probably why computer science people (supposedly) favor this naming. I might 
even use this naming myself when appropriate, although I'd say 'tuple' (or 
record) instead of 'product' to (hopefully) avoid confusion.

The sum-product naming, by contrast, comes from thinking about, we have n-ary 
sums and products for any natural n; for instance, A + B and A * B are binary. 
This can be viewed as sums and products of families of types indexed by finite 
sets. What if we generalize this to sums and products of families indexed by 
*arbitrary* types? Unlike the above, I don't think this is something that is 
likely to be sparked naturally during programming. However, it's quite close 
to similar constructions in set theory, which probably explains why 
mathematicians favor it.

If you get into category theoretic views of programming languages, I think the 
sum-product naming makes sense there, and it's hard to make the product-
function naming work. For instance:

  The A-indexed product Π x:A. F[x] has an A-indexed family of projections:
   proj a : (Π x:A. F[x]) - F[a]

  The A-indexed sum Σ x:A. F[x] has an A-indexed family of injections:
   in a : F[a] - (Σ x:A. F[x])

Which are visibly generalizations of the definitions of (co)products you'd 
encounter modelling non-dependently typed languages. Perhaps this is on the 
math end of things, though.

-- Dan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe