Dynamic Witnesses for Static Type Errors (or, ill-typed programs usually go wrong) by Eric L. Seidel, Ranjit Jhala, Westley Weimer:
Sounds like a great idea to make type systems more accessible, particularly for beginners. The current limitations are described the discussion, section 54:
It's also not clear whether this would produce proper witnesses for violations of higher kinded types or other more sophisticated uses of type systems. There are plenty of examples where invariants are encoded in types, eg. lightweight static capabilities.
How to Build Static Checking Systems Using Orders of Magnitude Less Code, by Fraser Brown Andres Notzli Dawson Engler:
Looks like an interesting approach with some compelling results, and will make a good tool for the toolbox. See also the Reddit thread for further discussion.
GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness by Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, Simon Peyton Jones:
Another great paper on a very useful incremental improvement on GADTs as found in Haskell, OCaml and Idris. Exhaustiveness checking is critical for a type system's effectiveness, and the redundant matching warnings are a nice bonus.
I am about to make some changes to the name server definitions. Since changes take time to propagate, you may have trouble reaching the site for awhile. If this happens, try using the .com domain instead of the preferred .org domain.
Lambda the Ultimate is now running on a new, faster, more reliable server. The old one is now, uh... pining for the fjords. This should resolve the increasingly frequent outages we've seen recently. Because the old server had started failing, we didn't have time to do as much quality control on the migration as we would have liked. If anyone notices any issues with the site, please comment in this thread. Currently known issues:
As many of you know we have been suffering for a long time from the deficiencies of Drupal. We have not updated our infrastructure for a long time. Among the features members have been asking for are better integration with other sites and more social features. In particular, many said they want to be able to mark the posts that they find particularly helpful. I am happy to announce that we have big news!
In the coming days we will be migrating LtU from Drupal to Facebook. All the awesome features of Facebook will be automatically available; in particular the "Like" mechanism. You will also be able to share photos with other PLT enthusiasts, re-share their shares etc. Best of all, you will be guaranteed the privacy standards of Facebook.
Rest assured, we have not made this decision without considering the alternatives. We studied Google+ but given Google's unprovoked assault on RSS with the decision to discontinue Google Reader we found it unconscionable to go with Google.
LtU's twitter feed will have to go, I am afraid, given the relationship between our new home and twitter. Hopefully this issue will be resolved once twitter gives up and is acquired by FB.
The LtU feed will have ads, per usual on FB. I know this is somewhat of an inconvenience, but at least the ads you will be served will be personalized.
Ehud and the LtU Team.
 I am assured that ads for dynamically typed and scripting languages will never be served to you again after you mark them as "offensive" once.
Earlier today I enabled a drupal feature that list the names of users currently online. It was on the bottom of the right-hand navigation bar, and looked something like this:
Some might see this as a privacy violation or otherwise object. Since I heard complaints I disabled this feature. What do you think?
Due to issues with spam accounts I have suspended the creation of new accounts. New members cannot sign up for an account at the moment. I apologize for the inconvenience.
So, LtU is 12!! I don't think this should go unnoticed. But as I was mostly quiet around here this year I am not qualified to offer a state of the lambda retrospective. Feel free to do so in the comments and, as they say, have some '(cake).
While ethics aren't normal LtU fare, it's sometimes interesting to see how our technical discussions fit into a larger picture.
In When Formal Systems Kill: Computer Ethics and Formal Methods February, 2012, Darren Abramson and Lee Pike make the case that the ubiquity of computing in safety critical systems and systems that can create real economic harm means that formal methods should not just be technical and economic discussions but ethical ones as well.
They also spend a good amount of time giving a lay overview of the practical, economic challenges faced by formal methods.
Active forum topics
New forum topics