Thanks for wasting half an hour of my life spent looking at blog postings about "spreadsheet functions" and "tying the knot" and "tautological containers". I fucking hate Haskell.
>>7
Don't like Haskell?
What's the matter? Too DEEP for you?
Name:
Anonymous2008-05-08 22:24
loeb [const "Hello", const "World", show]
Name:
Anonymous2008-05-09 7:22
In order to talk about whether or not a proposition is true we have to use some kind of Gödel numbering scheme to turn propositions into numbers and then if a proposition has number g, we need a function True so that True(g)=1 if g is the Gödel number of something true and 0 otherwise. But because of Tarski's proof of the indefinability of truth, we can't do this (to be honest, the argument above should be enough to convince you of this, unless you believe in Santa). On the other hand, we can replace True with Provable, just like in Gödel's incompleteness theorems, because provability is just a statement about deriving strings from strings using rewrite rules. If we do this, the above argument (after some work) turns into a valid proof - in fact, a proof of Löb's theorem. Informally it says that if it is provable that "P is provable implies P" then P is provable. We did something similar above with P="Santa Claus exists". In other words
□(□P→P)→□P.
So I'm going to take that as my theorem from which I'll derive a type. But what should □ become in Haskell? Let's take the easy option, we'll defer that decision until later and assume as little as possible. Let's represent □ by a type that is a Functor. The defining property of a functor corresponds to the theorem □(a→b)→□a→□b.
loeb :: Functor a => a (a x -> x) -> a x
So now to actually find an implementation of this.
Suppose a is some kind of container. The argument of loeb is a container of functions. They are in fact functions that act on the return type of loeb. So we have a convenient object for these functions to act on, we feed the return value of loeb back into each of the elements of the argument in turn. Haskell, being a lazy language, doesn't mind that sort of thing. So here's a possible implementation:
loeb x = fmap (\a -> a (loeb x)) x
Name:
Anonymous2008-05-09 7:41
SI(P[/spoiler])
Name:
Anonymous2008-05-11 11:09
someone should mail this thread to sigfpe, but i cnt find his email address
Name:
Anonymous2008-05-11 11:44
The monadic version is easier to understand.
loeb :: (Monad m) => m (m b -> b) -> m b
loeb x = fix (ap x . return)