GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness

GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness by Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, Simon Peyton Jones:

For ML and Haskell, accurate warnings when a function definition has redundant or missing patterns are mission critical. But today’s compilers generate bogus warnings when the programmer uses guards (even simple ones), GADTs, pattern guards, or view patterns. We give the first algorithm that handles all these cases in a single, uniform framework, together with an implementation in GHC, and evidence of its utility in practice.

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.

Domain settings

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.

LtU's new server

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:
  • Non-Latin UTF-8 characters apparently didn't survive the database migration correctly. This is a particular issue if you have a username containing non-Latin characters - you may not be able to log in currently.
  • It's possible that some comments posted later on Monday don't appear on the new site. (Resolved: there were no missing comments)
  • New user signup emails are not yet working.
  • Due to DNS propagation, not everyone will see the new site immediately. (Now resolved)
The struck out issues have been resolved. The remaining issue, with user signup emails, should be resolved in the next few days.

LtU is migrating from Drupal

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[1].

Ehud and the LtU Team.

[1] 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.

Update: No, we are not migrating to Facebook. This was an April Fools joke.

Who's online

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:

Who's online
There are currently 7 users and 887 guests online.
Online users:

Matt M
Ehud Lamm
Mattias Engdegård
Andreas Rossberg

Some might see this as a privacy violation or otherwise object. Since I heard complaints I disabled this feature. What do you think?

Setting up new accounts suspended

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).

When Formal Systems Kill: Computer Ethics and Formal Methods

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.

Computers are different from all other artifacts in that they are automatic formal systems. Since computers are automatic formal systems,techniques called formal methods can be used to help ensure their safety. First, we call upon practitioners of computer ethics to deliberate over when the application of formal methods to computing systems is a moral obligation. To support this deliberation, we provide a primer of the subfield of computer science called formal methods for non-specialists. Second, we give a few arguments in favor of bringing discussions of formal methods into the fold of computer ethics.

They also spend a good amount of time giving a lay overview of the practical, economic challenges faced by formal methods.

It's been ten years!

It has been ten years since LtU was launched. When I launched it I had no idea if anyone will read the site, let alone if people contribute new stories. The result exceeded my wildest hopes.

I got into the habit of writing a few words every year, a kind of "state of lambda" post. Somehow, this feels inappropriate for the ten year anniversary. I will possibly post something about last year later this week, but let's take a moment to celebrate our first ten years.

There are a lot of things that can be said, and a few things that perhaps should be said. I personally will say little. The thread is open.

For my part, I just want to thank all those how contributed to LtU over the years, whether by submitting new stories, by participating in the discussion, or with help with administrative and hosting issues. Some, of course, helped with any and all tasks.

It is great to see that some members that have been with LtU from its early years are still here. Some members that left have come back, and those that decided to move on to other things are still part of the ethos of LtU, as well as the archives, as we move towards the future.

The War on Spam

In recent weeks the volume of new spammer accounts has grown considerably. These accounts are sometimes used to post spam messages to the discussion group, but more often are simply used to game google by including spam urls in the user profile.

Due to the high volume of new spammer accounts I have implemented a new policy regarding new accounts. Given how things play out, it may become permanent:

1. New accounts are bocked by default, until released by an administrator. The user receives an email explaining this. While blocked, the user profile is invisible to anyone but the site administrators. They are also, of course, unable to sign in.

2. Accounts that seem legitimate, are released, while accounts that are clearly spam (e.g., from know spammers, include spam urls) are either deleted or put in the spammer category.

3. Accounts that we can't be sure about may be put in the "on probation" category. Members of this class can post, but their posts will appear only after being reviewed by an administrator. If the user turns out to be legitimate, it will be moved to the regular category, allowing the member to post directly.

4. Note that the "on probation" category is also used for members who are not spammers, but are considered or tend to post messages that are off topic. The messages posted by users that are on probation are in general reviewed by me before being allowed to appear.

New users are advised that by putting a short sentence or two about their specific interests relating to PL in their user profile, they will help us allow them to post sooner.

XML feed