Re: [Haskell-cafe] Re: Very freaky

On Tue, 10 Jul 2007, Aaron Denney wrote:

On 2007-07-10, Dan Piponi wrote:

...

On 7/10/07, Andrew Coppin wrote:

...

But what does, say, "Maybe x -> x" say?

Maybe X is the same as "True or X", where True is the statement that is always true. Remember that the definition is

data Maybe X = Nothing | Just X

You can read | as 'or', 'Just' as nothing but a wrapper around an X and Nothing as an axiom.

So Maybe X -> X says that "True or X" implies X. That's a valid proposition.

It is? Doesn't look like it. Unless you just mean "grammatical" by valid, rather than "true".

It's true in Haskell - undefined is a valid proof of anything you like, which is of course rather unsound. -- flippa@flippac.org A problem that's all in your head is still a problem. Brain damage is but one form of mind damage.