Why do you think that constructivists are against +0 /= -0?
Because they can't prove it - either way.
Or that they think that all functions are continuous?
[See previous email] Because all constructible functions are provably continuous.
Do you think that Per Martin-LÃf would a priori reject -0 as
a typed object ?
I would most definitely not want to put words in someone else's mouth!
However, if -0 exists, then it is likely that you'll be forced to have a `left' 1 and a `right' 1 (as well as every other number) too.
There are some physicists which have some bias towards constructivism,
since for them the Mathematical Nature of the Nature is constructive, the
sense of the word 'exist' is *not* so abstract...
Yet, they know that physical quantum amplitudes *must* have branch cuts
because of unitarity...
"branch cuts" require one to decide equality of reals - which constructivists reject, as that is a non-terminating process.
Having fun being off-topic, Jacques _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
