News for hackers. Stuff that matters.

A comment on Division by zero in type theory: a FAQ. Parent comment

Re:Division by zero in type theory: a FAQ by teraflop on Tuesday July 07, 2020 @02:42AM (#23756382)
Why would you want the product of two non-zero values to equal zero?

Among other things, this would have the unpleasant effect of making expressions like "0÷1" undefined, because the result could equal either zero or infinity.

[ Parent | on HN ]
Re:Division by zero in type theory: a FAQ by dependenttypes on Tuesday July 07, 2020 @10:30AM (#23759643)
Apologies, I meant for 0 * inf = 0. Since in n * inf n can be 0 the result should be able to be 0.
[ Parent | on HN ]
Re:Division by zero in type theory: a FAQ by somewhereoutth on Tuesday July 07, 2020 @03:06PM (#23762851)
You are correct - it should indeed be zero (and * can be constructed accordingly)
[ Parent | on HN ]