Stefan O'Rear wrote:
On Tue, Jul 10, 2007 at 08:19:53PM +0100, Andrew Coppin wrote:
So is this all a huge coincidence? Or have I actually suceeded in comprehending Wikipedia?
Yup, you understood it perfectly.
This is a rare event... I must note it on my calendar! o_O
This is precisely the Curry-Howard isomorphism I alluded to earlier.
Yeah, the article I was reading was called "Curry-Howard isomorphism". But it rambled on for, like, 3 pagefulls of completely opaque set-theoretic gibberish before I arrived at the (cryptically phrased) statements I presented above. Why it didn't just *say* that in the first place I have no idea...
Another good example:
foo :: ∀ pred : Nat → Prop . (∀ n:Nat . pred n → pred (n + 1)) → pred 0 → ∀ n : Nat . pred n
x_x
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.
...and to think the idea of mathematical symbols is to make things *clearer*...
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:
Peano integers are like Church numerals, but less scary. ;-) (I have a sudden feeling that that would make a good quote for... somewhere...)
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!
Error: Insufficient congative power.
http://haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence might be interesting - same idea, but written for a Haskell audience.
An interesting read - although again a little over my head. I find myself wondering... A polymorphic type signature such as (a -> b) -> a -> b says "given that a implies b and a is true, b is true". But what does, say, "Maybe x -> x" say?