Lambda the Ultimate

In connection with an effort to reason about numerical programs we recently ran into what seems to be strange decisions in the design of the floating-point standard, IEEE 754. I discuss the issues in a blog post ("Reflexivity and other pillars of civilization"), showing in particular that the convention for equality regarding NaN (Not A Number) seem wrong; the reverse convention would be more in line with basic mathematical properties such as the reflexivity of equality.

We encountered the problem in connection with the work on revising the ISO standard for Eiffel, when we realized that transposing the IEEE 754 rule to the language would mean that we cannot put a value into an array and then assume that the value that we put is there! Neither can we assign a value v to a variable x and assume that afterward the value of x is equal to v.

See the detailed explanation at the page linked to above. I would be interested in the experience of people having run into similar issues.

Hi! This is my first post, and I am just a Ph.D. student, so please be twice patient in case my question is really dumb.

I was wondering if anyone ever tried mixing monads (especially state/continuation monads) and object encodings to achieve an "Objective Haskell". This way we could get mutable objects which behave very closely to Java/C# ones and with a relatively similar syntax thanks to syntactic sugar for monads.

http://eliminatingwork.blogspot.com/2010/02/why-prolog-is-by-far-best-most.html

Prompted by Z-bo's question of what is there to gripe about CSS, I thought I'd point out the Clutter toolkit:

Clutter is an open source software library for creating fast, visually rich, portable and animated graphical user interfaces.

Clutter uses OpenGL (and optionally OpenGL|ES for use on Mobile and embedded platforms) for rendering but with an API which hides the underlying GL complexity from the developer. The Clutter API is intended to be easy to use, efficient and flexible.

Similar to Bling, it explores how GPU abstractions should be exposed to UI layout designers. I think there will be a lot of turmoil in this space over the next few years. Some related projects of interest are PixelBlender (with its integration into Flex 4) and similar projects in the Silverlight community. Another approach is to try to not change anything, as in a new GPU-accelerated Firefox branch. The only comparable approach I know of in the PL space is Conal Elliott's Vertigo, but that was not really about structured UI.

Edit: link fixed.

Edit 2: two big motivations here 1) performance on mobile devices and 2) enabling new types of UIs, such as physically realistic ones

I've just begun reading Whitehead and Russell's "Principia Mathematica" available here and was surprised to find on page 9 a nice readable alternative to parentheses for grouping.

Each operator is preceded and/or succeeded by some dots written as colons and periods. The more dots an operator has, the lower precedence it has. To take one of their examples (page 10),
p -> q .->. q -> r :->. p -> r
means
((p -> q) -> (q -> r)) -> (p -> r)

I find the dot version more readable and easier to type than the parentheses version. I'm curious if anyone here knows of other alternatives to parentheses for grouping. Prefix and postfix we've all heard of here, but do you have less well known ones? Hideous or beautiful I'd love to see them! Have any been tried in programming languages?

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.

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.

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:-)?

Is anybody aware of university courses (or textbooks) with a focus on the design of just-in-time compilers (JITs)? (Basically, as alternative to a standard compiler construction course)

In the last few years there has been some interesting research on the topic of JITs, (many being mentioned here on LtU), e.g., the Javascript JITs (TraceMonkey, Google V8), the PyPy JIT, LuaJIT, the recent story about verified JITs, Factor's compilation strategy might also be of interest, etc..

So far, I have not found any course focusing on JITs. At most, some compiler construction courses mention JIT technology (usually Java's) in passing. The textbook situation seems to be equally bland.

As a mathematician who's quite new to type theory, I have only vaguely internalised the fact that forall a.a and Pi a.a (or whatever the appropriate ASCII-isations are) mean the same thing. Thus, although it seems obvious to me that forall a.a is empty (or does one say uninhabited?), I was nonetheless quite startled to read the following in Barendregt's "Introduction to generalised type systems", p. 132:

… write \bot \equiv (\Pi \alpha : *. \alpha), which is the second-order definition of falsum.

I tried to re-cast this in language more familiar to me, and wound up with the statement that the product of all sets is empty.

Now, I know that type theories tend (understandably) to be biased more towards constructivist than traditional ZFC-based axiomatisations; but it seems to me that, beyond just saying that we don't assume the Axiom of Choice, this statement is saying that we take that axiom as the definition of ‘false’! Is the rejection of choosiness really so definitive, or am I just skipping over some point (like, say, that some sets are empty, so that including them in the product will naturally make it, too, empty)?