[Haskell-cafe] Very freaky

[Stefan O'Rear]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070710/6fddd6f6/attachment.bin