3 ms·

> Also, division by zero is an runtime operation error, it is not really a type error .. in most languages. This is not universally true however. Consider a la

> Also, division by zero is an runtime operation error, it is not really a type error .. in most languages. This is not universally true however. Consider a language with dependent types whose division function has a type signature like so: div : Nat -> (y : Nat) -> (y > 0) = True -> Nat, which basically requires a proof that can be verified at compile time that y is bigger than 0. In such a language you would not have a division by zero runtime error. You can even have something similar (but much more painful to use) in languages without dependent types, consider: data Nat1 = Succ Nat1 | One data Nat = CNat1 Nat1 | Zero div : Nat -> Nat1 -> Nat

jepler 8y ago
Ada is an example of a standardized, mature language with a "natural number" (strictly positive integer) type.
- tremon 8y ago
  But Ada doesn't restrict its division operators (div, mod and rem) to just "natural number" divisors.
josephg 8y ago
Right. You can also think of a type as a set of valid values that a variable could hold. In typescript you can define union types that simply hold one of a set of defined values. Eg: type OneOrThree = 1 | 3 or type Nullable<T> = T | null This is arguably nicer than Maybe / Option because you can loosen / tighten API constraints without changing the API. Eg, myfn(x: number) can be rewritten to myfn(x: number | null) with all the safety benefits of Maybe but without the need to change any callers. Its not just Ada - Rust also has non-zero integer types in the standard library. Eg: https://doc.rust-lang.org/std/num/struct.NonZeroU32.html https://doc.rust-lang.org/std/num/struct.NonZeroU32.html This was written mostly let Option<NonZeroU32> take up the same amount of space as u32. Ie, if you know your integer will never be zero, you can reuse the zero slot as a sentinal None value in a way thats API-compatible with everything else in rust.
- AnaniasAnanas 8y ago
  > You can also think of a type as a set of valid values that a variable could hold I would suggest avoiding this kind of thinking. Set theory and type theory are separate. Mixing them will only cause confusion and suffering. > without changing the API Pretty sure that loosening the return type constraints of a function or tightening the constrains of a variable that a function accepts would both change the API, is my understanding incorrect? > This was written mostly let Option<NonZeroU32> take up the same amount of space as u32 Why not just use u32 then? These are basically the same thing after all.
  - int_19h 8y ago
    > I would suggest avoiding this kind of thinking. Set theory and type theory are separate. There are some languages - notably, Ada - where this (types as sets) is very much explicit in the language. > Why not just use u32 then? For u32, 0 is "just another value" - there's nothing special about it. If you pass it to some other code, there's nothing telling them that they must check for zero, and must not treat zero as actual zero value (and if they forget, it will silently give the wrong answer). Option<NonZeroU32> requires them to pattern-match on None/Some, and if they get Some, it's guaranteed to be non-zero. That None is stored as zero is an implementation detail in that case, and doesn't leak onto the abstraction level on which code operates.

jepler 8y ago

Ada is an example of a standardized, mature language with a "natural number" (strictly positive integer) type.

tremon 8y ago
But Ada doesn't restrict its division operators (div, mod and rem) to just "natural number" divisors.

josephg 8y ago

Right. You can also think of a type as a set of valid values that a variable could hold. In typescript you can define union types that simply hold one of a set of defined values. Eg: type OneOrThree = 1 | 3 or type Nullable<T> = T | null This is arguably nicer than Maybe / Option because you can loosen / tighten API constraints without changing the API. Eg, myfn(x: number) can be rewritten to myfn(x: number | null) with all the safety benefits of Maybe but without the need to change any callers. Its not just Ada - Rust also has non-zero integer types in the standard library. Eg: https://doc.rust-lang.org/std/num/struct.NonZeroU32.html https://doc.rust-lang.org/std/num/struct.NonZeroU32.html This was written mostly let Option<NonZeroU32> take up the same amount of space as u32. Ie, if you know your integer will never be zero, you can reuse the zero slot as a sentinal None value in a way thats API-compatible with everything else in rust.

AnaniasAnanas 8y ago
> You can also think of a type as a set of valid values that a variable could hold I would suggest avoiding this kind of thinking. Set theory and type theory are separate. Mixing them will only cause confusion and suffering. > without changing the API Pretty sure that loosening the return type constraints of a function or tightening the constrains of a variable that a function accepts would both change the API, is my understanding incorrect? > This was written mostly let Option<NonZeroU32> take up the same amount of space as u32 Why not just use u32 then? These are basically the same thing after all.
- int_19h 8y ago
  > I would suggest avoiding this kind of thinking. Set theory and type theory are separate. There are some languages - notably, Ada - where this (types as sets) is very much explicit in the language. > Why not just use u32 then? For u32, 0 is "just another value" - there's nothing special about it. If you pass it to some other code, there's nothing telling them that they must check for zero, and must not treat zero as actual zero value (and if they forget, it will silently give the wrong answer). Option<NonZeroU32> requires them to pattern-match on None/Some, and if they get Some, it's guaranteed to be non-zero. That None is stored as zero is an implementation detail in that case, and doesn't leak onto the abstraction level on which code operates.