On Eq, was Re: [Haskell-cafe] When to use fancy types [Re: NumberTheory library]

[Jacques Carette]

karczma at info.unicaen.fr wrote:
> 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