Lambda the Ultimate

Why is doing type dispatch on method calls different or more acceptable to (static) type theorists than doing type dispatch on continuation (return) calls?

Function calls and function returns are completely isomorphic, as anyone can prove by transforming a program into continuation-passing style. What possible justification then, can there be for considering type dispatch "sound" and return dispatch "unsound"?

The more I think about this the more fundamental a question it seems to become.

The essence of sound static typing is that, at any point in the program, we know exactly what type everything is, yes? Without resorting to nasty labels like type tags, for the purists. We can achieve that in the presence of polymorphic function calls by choosing at what point in the program to continue based on what type/s we are returning.

There is no difference between this technique and choosing what point in the program to call based on the argument types, because after all every function return is just a function call to a continuation. In both cases, we know exactly what type everything is at every point in the program simply because we do not go to points in the program where the types we have in hand would result in a type mismatch with the types expected at that point in the program.

Syntactically some code may look like a ladder of type checks, but the clauses can be treated as separate continuation addresses to pass to the function whose type they are checking.

Okay, so it's Easter Sunday, and I feel a bit risen (in the sense of bread dough, that is — full of bubbles). What is more, I have finally made it through Learn You A Haskell, and in consequence I no longer fear The Monad.

Indeed, I found myself perpetrating the following little ditty, which I hereby share with other Haskell fans who are also fans of 42nd Street:

We're in the monad,
We're in the monad,
We've got a context that we have to pass along!
We're in the monad,
Our life's not so bad,
Well-typed imperative programming can't go wrong!

We never need to muta-
Te inscruta-ble state,
And when we see IO types
We can look those guys right in the eyes ...

We're in the monad
(Just rhymes with "gonad"),
Let's choose it, use it,
Keep it moving along!

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.