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

[Albert Y. C. Lai]

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.