Hacker News Reader

Comment by fao_ | Hacker News Reader

"Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero."

Zero is a different type from the type that consists of integers above N.

View on HN

What is "the type that consists of integers above N?" If N = -1, then 0 is in the set of integers greater than N.

I think it makes more sense to say that division is a function F × (F - {0}) → F where F is a field. F is not the same set/type as F without 0. I think in the context of computer languages this would be called a refinement type. (https://en.wikipedia.org/wiki/Refinement_type)

Can you show a language that implements your concept of "integers above N" consistently? I fail to see how such a type would be remotely useful in the context of addition/subtraction operators.

I think Ada comes closest to your definition with allowing modular and derived integer types, but the former does include 0 and I'm not sure if the latter even allows division.

Its an interesting concept. Addition or subtraction now would have to dynamically return either a zero type or a non-zero type. I suppose the type system could force you to check and handle the zero case.

In reality I think it would be too cumbersome. Division by zero is a relatively rare flaw and zero agnostic math on integers is common. I'd love to hear about any languages that do this.

Not necessarily, additional and subtraction just return int, but you can define other operations over subsets of ints that return nonzero.

Rust does something similar, floats by default can be NaN, but you can write a non-NaN float that just panics if it's Nan and then ignore the possibility of Nan in parts of your system.

Reply on news.ycombinator.com