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