User loginNavigation 
Category TheoryA Lambda Calculus for Real AnalysisA Lambda Calculus for Real Analysis
Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated JeanYves Girard's regrettably outofprint Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX. By Paul Snively at 20100216 22:00  Category Theory  Functional  Lambda Calculus  Logic/Declarative  MetaProgramming  Semantics  Type Theory  9 comments  other blogs  13366 reads
Simplicial DatabasesSimplicial Databases, David I. Spivak.
This is what happens when you try to take the existence of ORDER BY and COUNT in SQL seriously. :) If you're puzzled by how a geometric idea like simplexes could show up here, remember that the algebraic view of simplicial sets is as presheaves on the category of finite total orders and orderpreserving maps. Every finite sequence gives rise to a total order on its set of positions, and tables have rows and columns as sequences! An Innocent Model of Linear LogicAn Innocent Model of Linear Logic by PaulAndré Melliès was referenced by Noam in a serendipitious subthread of the "Claiming Infinities" thread. Here's the abstract:
The introduction goes on to refer to to André Joyal's "Category Y with Conway games as objects, and winning strategies as morphisms, composed by sequential interaction," and points out that "it is a precursor of game semantics for proof theory and programming languages," and is "a selfdual category of sequential games." The foreword mentions that the paper goes on to give "a crash course on asynchronous games" and then "constructs a linear continuation monad equivalent to the identity functor, by allowing internal positions in our games, [which] circumvents the Blass problem and defines a model of linear logic." Jacques Carette called this paper mindblowing. My mindblow warning light already exploded. I'm posting this paper because I know a number of LtUers are interested in these topics, and this way I can buttonhole one of them the next time I see them and ask them to explain it to me. ;) By Anton van Straaten at 20091218 03:23  Category Theory  8 comments  other blogs  12088 reads
Lawvere Theories and MonadsMartin Hyland and John Power (2007). The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads. ENTCS 172:437458. Both monads and Lawvere theories provide characterisations of algebraic structure, with monads providing the more general characterisation. The authors provide an introduction to Lawvere theories, discusses their relationship to sets, and why monads became the more popular treatment. Then they tackle the application of the theory to the semantics of side effects, where they argue that the generality of monads allow them to characterise computational phenomena that are not to do with side effects such as partiality and continuations, and argue that Lawvere theories more cleanly characterise what side effects are. This paper is a good introduction to an important line of recent research done by Hyland&Power; cf. also the LtU story Combining computational effects. Parameterized Notions of ComputationParameterized Notions of Computation, Robert Atkey, JFP 2008.
Once you've programmed with monads for a while, it's pretty common to start defining parameterized families of monads  e.g., we might define a family of type constructors for IO, in which the program type additionally tracks which files the computation reads and writes from. This is a very convenient programming pattern, but the theory of it is honestly a little sketchy: on what basis do we conclude that the indices we define actually track what we intend them to? And furthermore, why can we believe that (say) the monadic equational laws still apply? That's the question Atkey lays out a nice solution to. He gives a nice categorical semantics for indexed, effectful computations, and then cooks up lambda calculi whose equational theory corresponds to the equations his semantics justifies. The application to delimited continuations is quite nice, and the type theories can also give a little insight into the basics of how stuff like Hoare Type Theory works (which uses parameterized monads, with a very sophisticated language of parameters). On a slightly tangential note, this also raises in my mind a methodological point. Over the last n years, we've seen many people identify certain type constructors, whose usage is pervasive, and greatly simplified with some syntactic extensions  monads, comonads, applicative functors, arrows, and so on. It's incredible to suggest that we have exhausted the list of interesting types, and so together they constitute a good argument for some kind of language extension mechanism, such as macros. However, all these examples also raise the bar for when a macro is a good idea, because what makes them compelling is precisely that the right syntax yields an interesting and pretty equational theory in the extended language. By neelk at 20090211 21:40  Category Theory  Lambda Calculus  Semantics  Type Theory  16 comments  other blogs  12613 reads
Computation and the Periodic TableBy now there is an extensive network of interlocking analogies between physics, topology, logic and computer science, which can be seen most easily by comparing the roles that symmetric monoidal closed categories play in each subject. However, symmetric monoidal categories are just the n = 1, k = 3 entry of a hypothesized â€œperiodic tableâ€ of ktuply monoidal ncategories. This raises the question of how these analogies extend. We present some thoughts on this question, focusing on how monoidal closed 2categories might let us understand the lambda calculus more deeply. Arrows generalise monads and idioms
Two fresh papers from the Edinburgh theory stable:
Species: making analytic functors practical for functional programmingSpecies: making analytic functors practical for functional programming, Jacques Carette and Gordon Uszkay. Submitted to MSFP 2008.
Learning more about the theory of species and working out its implications for programming has been on my todo list for several years now. It really seems like the natural way to more tightly integrate combinatoric ideas into the functional programming style. (For an example of how fruitful this connection can be, consider how datatype differentiation explains zippers/functional pointers.) However, there's been this whole "graduation" and "primary research focus" stuff that's kept getting in the way, so I'm happy to see that Carette and Uszkay are figuring it out so I can just crib from them. :) Help 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  7618 reads

Browse archivesActive forum topics 
Recent comments
1 day 23 hours ago
2 days 5 hours ago
2 days 7 hours ago
2 days 17 hours ago
4 days 13 hours ago
5 days 20 hours ago
5 days 20 hours ago
1 week 17 hours ago
1 week 1 day ago
1 week 4 days ago