A student / friend had asked for examples of Haskell's Data.Void's utility during office hours and I was drawing a blank so I gave some wimpy "Oh, Dependent Programming uses them to express things like complete matches using set differences" having completely forgotten its real power. So I sent him:
While reading around the Internet today I was reminded of our conversation about Void and I, like a dunce, forgot an example that's vitally important: negation. (There are some others, too, [0] that are less interesting.)
Types and logic have a lot in common; every well-typed program is a proof in a constructive logic corresponding to its type system. The constructive form of the assertion "Not A" is actually "A implies Void", which has a natural type reading as an arrow type: a -> void (for a being the type corresponding to the proposition A).
That's all well and good, you're probably saying, but so what? So think of the Continuation Passing Style transform: every function of type a -> b becomes a function (a, b -> Void) -> Void, which we can read as "Not (A And Not B)" or "(Not A) Or (Not Not B)" or "A Implies (Not Not B)". The CPS transform works because we can freely introduce double negation in a constructive logic! In functional PL land, we can witness double negation introduction quite easily:
dni :: b -> ((b -> Void) -> Void) dni b notb = notb b
Logically, this corresponds "Hey, you told me that both B and Not B were true! Time to end the world." "End the world" here, however, in CPS, is a clever slight of hand for "returning to the caller" -- it ends *the callee's* world, to be sure.
The reverse, incidentally, is not true! Double-negation elimination's type would be "dne :: ((b -> Void) -> Void) -> b". But that's pretty useless. There's no way to conjure a function of type "b -> Void" to feed the argument and it wouldn't do us a whole lot of good even if we could.
However, there's a really amazing thing called "call with current continuation" in some languages, which has type (roughly; we can gloss over some details [2]) "callcc :: ((a -> Void) -> a) -> a". What does this do? Well, it takes a function "f" which *either* returns something of type a, in which case callcc returns that, or f invokes its argument with something of type a, in which case callcc returns *that*! Can you see how to make dne from callcc?
More generally, callcc is essentially... the power to prove by negation! Amazing... what?! callcc says "If you can give me a proof strategy (function) which can take Not A and prove A, then I can prove A". That is, if you provide a contradiction, callcc will provide the proof you wanted all along.
There's a story about a time travelling oracle here to tell, but perhaps it can wait.
[0] Broadly, any time you have a polymorphic function returning a something of a type variable that isn't mentioned anywhere else, you could instantiate it as Void and not alter the program's meaning or behavior (under assumptions [1]). Why? Because there's no way for the function to construct something type "forall a . a" (and given that the variable isn't mentioned anywhere else, we may as well shuffle the forall to the right of the arrow).
[1] Well, ahem, there are certain *rather alarming* exceptions, like the OCaml demarshaling library, which essentially has a function of type Representation -> String -> a. In Haskell we'd probably use a GADT with phantom argument, "Representation a", but OCaml didn't have those.
[2] callcc is an alarming construct from the perspective of a language implementer who has efficiency on the mind! It grabs the current (logical) stack frame and makes it a variable that's live in the program! The program could do things like store it into data structures (to make a cooperative thread scheduler, even! This is one of the assignments in CMU's second PL class)... or return it up the stack (oh *dear*) and invoke it later (resurrect finished worlds with fresh information; maybe it will go differently this time!) There *are* ways of dealing with this, but they're somewhat slow (necessitating, essentially, copy-on-write stacks; never know if someone's about to re-invoke a past continuation... this construction is sometimes called a "cactus stack"); so usually one sees ST-monad-like type stunts for delimiting liveness of callcc continuations. |