by **bitwiseshiftleft** » Wed Jun 13, 2007 9:46 pm UTC

Er. So yeah, sorry to be confusing. This isn't actually Haskell-inspired, but rather CS-theory-inspired.

A continuation is a function (in the programming sense, not in the strict mathematical sense) that takes some value and doesn't ever return. They're used a lot in Scheme. They're usually written k, which is why I said [k]ontinuation. So if you say that not returning is like "false", a continuation taking an x has type x->False, which is to say, !x (the ! means not here, since I was too lazy to find the unicode negation sign).

Either is a library function in a lot of functional languages. It takes a function taking an x, a function taking a y, and an x|y, and then invokes the appropriate one. It has type (x->z) -> (y->z) -> (x|y) -> z, which is a pretty obvious logical statement. I'm taking it as a primitive, because I haven't defined another way to extract values from x|y. More on that later.

Fst takes a pair and returns the first element, and so has type (x&y) -> x; similarly, snd is (x&y) -> y.

L and R have types x->x|y and y->x|y, respectively.

∘ (supposed to be the o-shaped "compose" operator, in case there are Unicode issues) composes two functions: f∘g = λx . f (g x). It has type (y->z) -> (x->y) -> (x->z).

You don't want to show that x&y -> x|y, because that's obvious (L∘fst and R∘snd both suffice). Rather, you want to show that !(x&y) -> !x | !y.

I talked to a friend about this the other day; apparently the reason that it's hard to write this function is that usually | is defined as x|y == !(!x&!y), but I'm making it primitive instead (this makes either unnecessary). That means that another function, most likely Scheme's call/cc (of type !!a -> a) is required. As it happens, call/cc expands the Curry-Howard isomorphism from intuitionistic logic to classical logic (I'm not a logic buff, so I'm not sure what the distinction is, other than that in intuitionistic logic !!a doesn't imply a), while the standard definition of | doesn't. I don't know why. Wikipedia probably does.

And no, this isn't homework.