Computing without a middle

Here’s an uncontrived scenario:

You have just recieved two Haskell modules from Microsoft (so there’s no way you will ever get the source). One of the modules is called Greeter, the other called MeaningOfLife. MeaningOfLife was written by God, for his own record keeping, in case he ever forgot. The rumor is that Microsoft purchased a portal from hell to heaven and sent spies to recover the MeaningOfLife module from him.

God doesn’t call himself “God”. He has a private name, and only he and his wife the “virgin” know it. God has another module, which he keeps locked up in a divine safe, which is a function that returns the encryption key for the meaning of life when given his name as input. Its type signature is:

    getEncryptionKey :: Name -> Divine EncryptionKey

(God keeps all of his computations in the Divine Monad)

You don’t have access to that function, all you have is the seemingly useless user interface function:

    getMeaningOfLife :: (Name -> Divine EncryptionKey) -> Divine String

This function asks for the user’s name, and sends it to the encryption key function which it has been passed, and returns the meaning of life. But it’s even more hopeless for you: you can’t even brute force it, for Name and EncryptionKey are both abstract data types to which you do not have the internal representations.

Discouraged, you look at the other module that Microsoft sent you, Greeter. It was also recovered during the spy mission, one of God’s first Haskell programs when he was learning. It has a single function, which, given the user’s name, friendlily says hello to the user:

    greet :: Name -> Divine ()

But again, you are out of luck, for Name is abstract and we don’t know how to make one.

It seems we are at an impass. We cannot run any of the new code we received, even just to test it, because we cannot create the encryption key generating function for getMeaningOfLife, and we cannot generate names for greet! What do we do?

Why, what’s this? A recent thread on Haskell Cafe explains that the law of excluded middle can be encoded in haskell’s type system as:

    exmid :: (MonadCont m) =>  m (Either (a -> m b) a)

That is, exmid asserts the existence of either a type a or a function which takes an a and returns anything you want. You could use this if only Divine was an instance of MonadCont. Looking in the docs, you are surprised to find that it is! Of course it is; God has the power to go back in time if something happens that he doesn’t like (in fact the “red button” that begins nuclear war actually just invokes the Modern Age continuation so we can try again. It’s like the reset button on your Nintendo.).

And this provides just what we need. We can finally have the meaning of life! Just:

    divineMain :: Divine ()
    divineMain = do
        em <- exmid                  -- get the function of excluded middle
        case em of
            Right name -> do         -- either a Name exists
                greet name
            Left fn ->  do           -- or a function taking names to Divine EncryptionKeys exists
                putStrLn "Get ready for it: Ready?  Here's the meaning of life!"
                meaningOfLife <- getMeaningOfLife fn
                putStrLn meaningOfLife

(The liftIOs have been omitted for readability)

Your heart racing, you run the program:

Get ready for it: Ready? Here's the meaning of life!
What is your name?  Luke
Hello, Luke, have a nice day.

And it worked! It actually worked! You were friendlily greeted (if you are me).

What happened here is that exmid certainly could not create a Name, how would it have the power to do so? So it couldn’t take the Right branch. All that was left to do is to take the Left branch, coming up with a fake function that claimed to satisfy what was asked of it (in this case, taking a Name to an EncryptionKey), in hopes that it wouldn’t be called (then exmid would get off clean easy). But when we passed that function to getMeaningOfLife, getMeaningOfLife did call it. Exmid noticed that this fake function that it created was passed a Name, which it was previously unable to conjure. Never one to miss an opportunity, exmid jumped back in time and took the Right branch instead, passing the right branch its newly acquired Name.

Put less anthropomorphically, using exmid we glued greet into the “middle” of getMeaningOfLife, where it was least expecting it (okay, I guess that was still anthropomorphic).

So there you have it, the Curry-Howard law of excluded middle is useful; it’s not all abstract theoretical gobbledygook.

For reference, the implementation of exmid follows, some dense abstract theoretical gobbledygook:

   exmid :: (MonadCont m) => m (Either (a -> m b) a)
   exmid = exeither' exmid'
       exmid' f g = either return g =<< callCC (\cc ->
                              return . Left =<< f (cc . Right))
       exeither' e = e (return . Left) (return . Right)

4 thoughts on “Computing without a middle

  1. Rereading Wadler’s duality paper presents an interesting study of contrasts. The jaded, time-worn professor writes about a billion dollars, the devil, and the ruin of one’s soul. The writing’s highly edited, the narrative’s sinewy and tight, classy with punch.

    The young whippersnapper whistles an extemporized tune about the meaning of life in lowerCamelCase, as safe-guarded by G-d who just happens to have a (only one?) virgin wife (there is an only son, see if you can spot him). Tickled pink by God giving him a friendly greeting, our hero is a happy camper endlessly amused with abstract theoretical gobbledygook.

    Devils, I suppose, were children once.

  2. An alternate implementation of exmid, which (possibly) makes it clearer exactly what it’s doing, is

    exmid = callCC (\cc -> return (Left (\x -> cc (Right x))))

    That is, at first exmid says, “I contain a value of type a -> m b.” But if anyone ever tries to call that function on a value of type a, exmid says, “I changed my mind; actually I contain a value of type a. And here it is!”

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s