At the end of section 4 of
Call-by-value is dual to call-by-name, Wadler tells a story about the Devil and a billion dollars. After a long time thinking about it, the meaning of it suddenly hit me like an epiphany a few weeks ago, and I'm finally in a position to give an explanation of what it means. (This is also an exercise in
TMR6.) And just for a bit of variety I'm going to throw in some C++ and Scheme, starting with some simple C++ code:
#include <iostream>
#include <string>
using namespace std;
template<class A,class B>
class Either
{
public:
virtual B value() const throw (A) = 0;
};
template<class A,class B>
class Left : public Either<A,B>
{
A a;
public:
Left(A a0) : a(a0) { }
B value() const throw (A) { throw a; }
};
template<class A,class B>
class Right : public Either<A,B>
{
B b;
public:
Right(B b0) : b(b0) { }
B value() const throw (A) { return b; }
};
template<class A,class B,class C>
C either(const Either<A,B> &e,C (*f)(A),C (*g)(B))
{
try {
return g(e.value());
} catch (A &a) {
return f(a);
}
}
string f(int a)
{
return "int";
}
string g(float b)
{
return "float";
}
int main()
{
std::cout <<
either<int,float,string>(Left<int,float>(7),f,g)
<< std::endl;
std::cout <<
either<int,float,string>(Right<int,float>(7.0f),f,g)
<< std::endl;
}
This provides a (somewhat unreliable, I think) implementation of a discriminated union. An object of type
Either<A,B> is either an object of type A or an object of type B. But unlike the ordinary union, it remembers the type of its contents. I've also provided an
either function. Given a function of type A→C and a function of type B→C, then if we're handed an object of type
Either<A,B> we know that we can apply one or other function to it to get an object of type C. The functon
either applies the appropriate one for you. What's unusual is the way I've implemented it. I'm representing an object of type
Either<A,B> as a function of no arguments (in effect a lazy value) returning something of type
B (*)() throw (A). There are two paths by which an object can get out of such a function: either it is returned or it is thrown out. Having two paths is what I've used to implement of a template that represents either one thing or another. This simple example should make it clear that there is some sort of a connection between exceptions and logical or (ie. disjunction).
In functional languages exceptions tend to be handled a little differently. Whereas C++ has a
throw keyword, there is no equivalent in Scheme, say. Instead
the
call-with-current-continuation function acts like
catch. The argument to
call-with-current-continuation is a function
(lambda (throw) ...) and the argument to this function (itself a function), here called
throw, does the throwing. For example consider the scheme expression:
(call-with-current-continuation
(lambda (throw) (+ 1 (throw 7))))
The result is 7, not 8. The 7 is thrown 'past' the
(+ 1 ...) and is caught by the surrounding
call-with-current-continuation. The important difference from C++ is that if any subexpression is to throw some value, it must be 'handed' a suitable throw function. Note also that Scheme is dynamically typed. In a static functional language throwing exceptions is a tiny bit more subtle. Not only must a subexpression be handed a suitable function for throwing, it must be handed a function of a suitable type. In particular, if the data thrown is to be of type a, then the subexpression must be handed a suitable 'throw' function that can take an object of type a as argument. Think of such a function as an a-consumer. So if we want to implement the C++ idea above in a statically typed functional language that supports exceptions we need to replace the function of type
B (*)() throw (A) with a function that consumes an A-consumer and returns an object of type B. Such a function can either throw a result of type A or return a result of type B.
Anyway, here's a complete Scheme example (BTW it's my first bit of Scheme code longer than one line):
(define (right b) (lambda (throw) b))
(define (left a) (lambda (throw) (throw a)))
(define (compose f g) (lambda (x) (f (g x))))
(define (id x) x)
(define (either f g x)
(call-with-current-continuation
(lambda (throw)
(g (x (compose throw f))))))
(define (f x) (cons "left" x))
(define (g x) (cons "right" x))
(either f g (left 1))
(either f g (right 2))
OK, time for some logic.
As everyone familiar with propositional calculus knows, a ∨ b = ~a → b. Or in English "a or b" is the same as "if a isn't true then b is".
Less well known is the Curry-Howard isomorphism. In a nutshell it goes like this: if you know a, and you know a → b, then you can deduce b (using modus ponens). Similarly, in a strictly typed programming language, if you have an object of type a, and a function of type a → b, then you can use them to make an object of type b (just apply the function to a). So given a bunch of propositions in 1-1 correspondence with a bunch of objects, you should be able to see that the set of propositions you can deduce by modus ponens is going to be in 1-1 correspondence with the objects you can make by function application.
But there's more to logic than modus ponens. In classical logic you also have double negation elimination. In other words, if you know ~~a then you can deduce a. So double negation elimination is like having a polymorphic function ~~a → a for any a. What does "~" mean in terms of functions? In logic, define ⊥ to be the unprovable false proposition. Then ~a is simply a→⊥. In programming define ⊥ to be the type with no instances and we can define ~a to be the type of functions a→⊥. A function of type ~a is a function that consumes an instance of type a and gives you back nothing in return. Clearly if you can make an object of type a then no function of type ~a can exist or else you could apply it to a and get an object f type ⊥, which is impossible by definition.
It's not hard to see that there can be no well behaved function that for any type a can map an ~~a to an a. An ~~a is a thing that consumes a-consumers. In a sense it's destructive. There are no raw ingredients from which you could possibly make an a for all a. So there is no
function of type ~~a → a. But this type can serve very well as the type of the
catch operator described above. Rewriting the scheme example above with Haskell-like notation we expect something like
catch $ \throw -> ... (throw a) ...
Because
throw never returns we can assign it the type
a -> ⊥ without problems and hence
catch can be assigned type ~~a. This now means that the Curry-Howard isomorphism can be extended to classical logic if we throw in
catch along with the usual functions you expect in a pure typed functional language.
So If we use
catch to throw an exception out of a function, then the function must be handed a ~a as argument. So in order to implement
Either, we must replace the C++ type
B (*)() throw(A) with
~a -> b. In other words, if we use the symbol ∨ to mean
either, then exactly in classical logic, we have a ∨ b = ~a → b.
You can think of the argument to
catch as being a bit like a bungee cord with one end attached to the
catch. If a function is handed the other end of such a bungee cord it can either use it to catapult out a value of type a, or the function can ignore it and return somehing of type b. But there's a neat twist on this. If b = ~a then the function, on being handed a bungee cord, could simply hand it back as a return value. In other words, whatever type a is, we can always construct an object of type a ∨ ~a from the identity function. This corresponds to the fact that a ∨ ~a is a tautology of classical logic.
And now you can reread Wadler's story about the Devil and see that my story about a bungee cord is really the same one.
Exercise: Implement Left, Right and either using the method above in the Haskell Cont monad.
PS Reasoning about exceptions in this way is new to me and so I don't feel I have the above on a firm footing. So expect some errors. In particular I haven't thought about what happens if you try to nest disjunctive structures this way. You can be sure that the C++ implementation will fail because the exception may be caught by the wrong
try.
Update: fixed some typos. But also here's an exercise:
Exercise: a ∧ b = ~(~a ∨ ~b). What does that mean in the above context? (I haven't got my head around this yet.)
Labels: types
