[Haskell-cafe] Re: Very freaky

Philippa Cowderoy flippa at flippac.org
Wed Jul 11 18:31:15 EDT 2007


On Tue, 10 Jul 2007, Aaron Denney wrote:

> On 2007-07-10, Dan Piponi <dpiponi at gmail.com> wrote:
> > On 7/10/07, Andrew Coppin <andrewcoppin at btinternet.com> 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 at flippac.org

A problem that's all in your head is still a problem.
Brain damage is but one form of mind damage.


More information about the Haskell-Cafe mailing list