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?
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
