[Haskell-cafe] Re: Wikipedia on first-class object

[Lennart Augustsson]

There's no (valid) formalism that says that [n..]==[n..] is True.
The formalism says that [n..] and [n..] are equal.  But being equal does not
mean that the Haskell (==) function returns True.
The (==) function is just an approximation of semantic equality (by
necessity).

  -- Lennart

On Dec 28, 2007 3:38 AM, Albert Y. C. Lai <trebla at vex.net> wrote:

> Achim Schneider wrote:
> > [n..] == [m..],
> >
> > the first thing I notice is
> >
> > n == m && n+1 == m+1
> >
> > , which already expresses all of infinity in one instance and can be
> > trivially cancelled to
> >
> > n == m
> >
> > , which makes the whole darn thing only _|_ if n or m is _|_, which no
> > member of [n..] can be as long as n isn't or 1 or + has funny ideas.
> >
> > I finally begin to understand my love and hate relationship with
> > formalisms: It involves cuddling with fixed points while protecting
> > them from evil data and fixed points they don't like as well as
> > reduction strategies that don't see their full beauty.
>
> There is a formalism that says [n..]==[n..] is true. (Look for
> co-induction, observational equivalence, bismulation, ...)
>
> There is a formalism that says [n..]==[n..] is _|_.
>
> We know of implemented programming languages that can give an answer
> according to the latter formalism.
>
> If you know of an implemented programming language that can give an
> answer according to the former formalism, and not just for the obvious
> [n..] but also map f xs == map g xs (for example), please spread the news.
>
> So it comes down to which formalism, not whether formalism.
>
> I have long known the problem with informalisms. They are full of "I
> know", "obviously", and "ought to be". It is too tempting to take your
> wit for granted. When you make a deduction, you don't easily see whether
> it is one of a systemtic family of deductions or you are just cunning.
> You only see what you can do; you don't see what you can't do, much less
> what you can't make a computer do.
>
> Formalisms do not tolerate such self-deception. You think something
> ought to be obvious? Write them down as axioms. Now with all your
> obviousness nailed down black on white, you have a solid ground on which
> to ask: what can be done, what can't be done, what can be done on a
> computer, how practical is it? Humility and productivity are thus
> restored.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071228/2556114a/attachment.htm