On Tue, Jul 10, 2007 at 08:19:53PM +0100, Andrew Coppin wrote:
OK, so technically it's got nothing to do with Haskell itself, but...
I was reading some utterly incomprehensible article in Wikipedia. It was saying something about categories of recursive sets or some nonesense like that, and then it said something utterly astonishing.
By playing with the lambda calculus, you can come up with functions having all sorts of types. For example,
identity :: x -> x
add :: x -> x -> x
apply :: (x -> y) -> (y -> z) -> (x -> z)
However - and I noticed this myself a while ago - it is quite impossible to write a (working) function such as
foo :: x -> y
Now, Wikipedia seems to be suggesting something really remarkable. The text is very poorly worded and hard to comprehend, but they seem to be asserting that a type can be interpreted as a logic theorum, and that you can only write a function with a specific type is the corresponding theorum is true. (Conversly, if you have a function with a given type, the corresponding theorum *must* be true.)
For example, the type for "identity" presumably reads as "given that x is true, we know that x is true". Well, duh!
Moving on, "add" tells as that "if x is true and x is true, then x is true". Again, duh.
Now "apply" seems to say that "if we know that x implies y, and we know that y implies z, then it follows that x implies z". Which is nontrivial, but certainly looks correct to me.
On the other hand, the type for "foo" says "given that some random statement x happens to be true, we know that some utterly unrelated statement y is also true". Which is obviously nucking futs.
Taking this further, we have "($) :: (x -> y) -> x -> y", which seems to read "given that x implies y, and that x is true, it follows that y is true". Which, again, seems to compute.
So is this all a huge coincidence? Or have I actually suceeded in comprehending Wikipedia?
Yup, you understood it perfectly. This is precisely the Curry-Howard isomorphism I alluded to earlier. Another good example: foo :: ∀ pred : Nat → Prop . (∀ n:Nat . pred n → pred (n + 1)) → pred 0 → ∀ n : Nat . pred n Which you can read as "For all statements about natural numbers, if the statement applies to 0, and if it applies to a number it applies to the next number, then it applies to all numbers.". IE, mathematical induction. Haskell's type system isn't *quite* powerful enough to express the notion of a type depending on a number (you can hack around it with a type-level Peano construction, but let's not go there just yet), but if you ignore that part of the type: foo :: (pred -> pred) -> pred -> Int -> pred {- the int should be nat, ie positive -} foo nx z 0 = z foo nx z (n+1) = nx (foo nx z n) Which is just an iteration function! http://haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence might be interesting - same idea, but written for a Haskell audience. Stefan