User loginNavigation 
Category TheoryHelp John Baez and Mike Stay!John Baez and Mike Stay are working on a book chapter titled "Categories in Physics, Topology, Logic and Computation: a Rosetta Stone." They previously asked for some help with the logic section, and now they're looking for help with the computation section:
This is already a great introductory paper, but the computation section is indeed quite rough. Obviously comments are welcome, but even if you don't have anything to add, the first sections are sure to be enjoyable for many LtU readers. The paper does not assume any background in category theory, logic or physics and manages to be an excellent introduction to the surprising connections between these fields. If you have some background, it's a very quick and fun read, and if you can offer feedback, so much the better! Parametric datatypegenericity
Parametric datatypegenericity. Jeremy Gibbons and Ross Paterson. Submitted for publication.
Datatypegeneric programs are programs that are parametrized by a datatype or type functor. There are two main styles of datatypegeneric programming: the Algebra of Programming approach, characterized by structured recursion operators parametrized by a shape functor, and the Generic Haskell approach, characterized by case analysis over the structure of a datatype. We show that the former enjoys a kind of parametricity, relating the behaviours of generic functions at different types; in contrast, the latter is more ad hoc, with no coherence required or provided between the various clauses of a definition. How could we have not mentioned this before? The main result of this paper is that fold is a higherorder natural transformation. This means, the authors explain, that fold is a rather special kind of datatypegeneric operator, both enjoying and requiring coherence between its datatypespecific instances. We had several long discussions about the uniqueness of fold, which may serve as an introduction for those new to this sort of discussion. The tutorial on the universality of fold is, of course, on the papers page. For some reason I feel a craving for bananas... By Ehud Lamm at 20071204 07:24  Category Theory  Functional  6 comments  other blogs  8544 reads
A Logic for Parametric PolymorphismA Logic for Parametric Polymorphism, Gordon Plotkin and MartÃn Abadi.
By neelk at 20070413 22:27  Category Theory  Lambda Calculus  Semantics  Theory  login or register to post comments  other blogs  6918 reads
A Topos Foundation for Theories of PhysicsA Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.
This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind. Via The nCategory Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"... By Matt Hellige at 20070321 05:13  Category Theory  Type Theory  8 comments  other blogs  9138 reads
Propositions as [Types]Propositions as [Types], Steve Awodey and Adrej Bauer.
I figure I should say a few words about why proof irrelevance is an interesting idea. In math, you often want to consider elements of a certain type that have certain properties  for example, you might want the set of satisfiable boolean formulas as part of a proof as a hypothesis of a theorem. The way you might represent this in dependent type theory is by giving a pair, consisting of a formula and a satisfying assignment. You might write this as One way of addressing this problem is to treat the second component of the pair as a proof irrelevant type. The basic idea is that for each type I should also add that this is an old idea in type theory; this is the paper that made it clear to me. (Thanks to Bob Harper for suggesting clarifications to my comments.) By neelk at 20070303 19:19  Category Theory  Type Theory  5 comments  other blogs  6839 reads
Using Category Theory to Design Implicit Conversions and Generic OperatorsUsing Category Theory to Design Implicit Conversions and Generic Operators, John C. Reynolds, 1980. (Try this if the official link doesn't work.)
This is an old, but still cute, paper. The basic intuition is that a good design principle for a language with implicit conversions is that whatever order of conversions the language takes, you should get the same result. He then formalizes that by giving a category of types and conversions, and demanding that everything commute properly. And these give just the conditions the language designer has to check to make sure that he or she hasn't screwed anything up. Someone could probably get a fun little paper by taking this idea and shooting some dependent types into it. (Maybe somebody already has?) If you've got an abstract type, a coercion function, and a proof that it satisfies Reynolds' conditions, now your compiler can silently insert those coercions for you as needed, but you can still be sure that it won't mess up the meaning of your program. Holodeck games and CCCsFrom the nCategory Cafe, some notes on Holodeck Games and cartesian closed categories. This also appeared here (and was mentioned by Phil Wadler). The two posts seem to have different addenda, comments and links, so it may be worth looking at both. It's fun to see lambda calculus introduced to an audience already familiar with categories, as that seems to be the opposite of the usual state of affairs around here, and I can think of certain LtU regulars who will hopefully find this whole subject enjoyable. By Matt Hellige at 20061023 23:03  Category Theory  Fun  Lambda Calculus  login or register to post comments  other blogs  6943 reads
Arrows, like Monads, are MonoidsBy Chris Heunen and Bart Jacobs
By Jim Apple at 20060930 19:04  Category Theory  Functional  Lambda Calculus  3 comments  other blogs  11234 reads
Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach
By Jim Apple at 20060909 12:34  Category Theory  Functional  login or register to post comments  other blogs  8957 reads
Socially Responsive, Environmentally Friendly LogicSocially Responsive, Environmentally Friendly Logic
This paper seems to unify multiple interesting directions  logic, game semantics, concurrent constraint programming (and concurrent programming in general). At the same time it remains very accessible, without overwhelming amount of math, so can be hopefully useful not only for academics. I, for one, was waiting for exactly this kind of paper for two years (and my interest is very practical). Multiplayer CurryHoward correspondence, anyone? Or CurryHoward for web services? By Andris Birkmanis at 20060710 17:28  Category Theory  Logic/Declarative  Semantics  10 comments  other blogs  9817 reads

Browse archivesActive forum topics 
Recent comments
3 hours 56 min ago
8 hours 45 min ago
16 hours 10 min ago
1 day 3 hours ago
1 day 8 hours ago
1 day 9 hours ago
1 day 9 hours ago
1 day 10 hours ago
1 day 10 hours ago
1 day 11 hours ago