[Haskell-cafe] Very freaky

[Andrew Coppin]

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?