Lambda the Ultimate

As I started learning category methods, I noticed that my prior attitude dismissing it as "abstract nonsense" was based upon ignorance. As somebody with physics background I begin to appreciate shifting emphasis from objects onto symmetry, invariance (err morphisms). So in order to understand structure one has to master morphisms. Fine.

Let's compare this with algebraic perspective. There we study objects and operations between them. When we constrain those operations with some axioms we get an algebraic system. A significant part of studying a concrete algebra would be discovering its axiom system. For example, Relation Algebra has been discovered by Pierce, but hasn't been fully axiomatized until Tarski.

Now, how would I study Relation Algebra with methods of category theory? As discovery is significant element of algebraic method and category theory is in a sense dual perspective, I'd guess drawing arrows wouldn't advance me too much, and I would have to discover some important morphisms... Perhaps, a helpful analogy would be how is it done in other categories (preferably, from elementary mathematical fields:-)?

Lunascript, our in-house language for writing great web apps:

Inspired by incremental computing, we're building Lunascript as a simple way to write modern web applications. Lunascript has a syntax and easy of use reminiscent of JavaScript, but a powerful pure-functional lazily-evaluated semantics historically confined to academic languages.

A Lunascript application specifes a data model and a function from the model to the view or user interface, annotated with handler functions from user inputs to model mutations. From this the Lunascript compiler produces a functioning Web2.0 application -- the client-side JavaScript, the server-side SQL, and everything in between -- complete with real-time bidirectional data synchronization.

I'll have to wait for more info on this definitely interesting project, but right now I'm a bit sceptical, as this seems to throw REST out the window.

Continuity Analysis of Programs, Swarat Chaudhuri, Sumit Galwani, and Roberto Lublinerman. POPL 2010.

We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the robustness of programs whose inputs can have small amounts of error and uncertainty -- e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data.

Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate “synchronization points” between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.

We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.

Another fun paper from POPL this year. I've seen metric spaces used to solve domain equations before, but the idea of actually considering a metric on the outputs was a new one to me.

I am looking for any papers that analyze the design of cascading stylesheets with respect to bounded times. I could derive this myself, but it would be nice to have a peer reviewed authority. It would also be cool if anyone ever bothered to do this for Hakon Wum-Lie's original CHSS (Cascading HTML Style Sheets) and Bert Bos's original SSP (Stream-based Style Sheet Proposal) prior to them being merged into CSS 1.0. Also, Dynamic Properties that were in Internet Explorer from 5.0 through 7.0, but deprecated in 8.0.

The only thing I found so far was a webpage: CSS, selectors and computational complexity. However, this doesn't communicate the complexity on how selectors place solving constraints on the layout engine to update each widget's CSS box model.

I'm also interested in knowing if anybody has done anything to model compatibilities across browsers. All I found was this (mindblowing) Comparison of layout engines and their support for CSS.

I don't think anyone has actually done anything to formally investigate the most widely used DSL in the world and the affect it has on clockcycles as well as programmer man-hours...

Thanks.