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' where exmid' f g = either return g =<< callCC (\cc -> return . Left =<< f (cc . Right)) exeither' e = e (return . Left) (return . Right)