[Haskell-cafe] Very freaky
andrewcoppin at btinternet.com
Tue Jul 10 15:19:53 EDT 2007
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
More information about the Haskell-Cafe