Is this a type error?

What is a type error?

Let’s say this is an error when the operation is applied to the value of the wrong type. For example, is division by zero a type error?

If we define division type signature as (Number, Number) -> Number than it is not a type error. But on the other hand, the division is a partial function e.g. it is not defined for all possible inputs (denominator can’t be zero). So to make the proposed type signature work we need to throw an exception (for undefined behavior). Example in Python:

1print(1/0)
2# ZeroDivisionError: integer division or modulo by zero

If we define division type signature as (Number, Number) -> Number | Undefined, we could use Undefined to represent the undefined behavior of the function. Now there is no exception nor type error when we call the function with zero, but instead, we need to do a “type check” of the result:

1if (result != Undefined) {
2  // now we know that result is Number
3}

If we define division type signature as (Number, NumberExceptZero) -> Number, we will make division by zero a type error.

Edge case handling

…in partial functions

Exception

Type signature: divide :: (Number, Number) -> Number

Throwing exception would make types correct because instead of getting an “undefined” value we will jump to a different branch of code, which means that function will either return the correct value or consequent instructions will not run.

1try {
2  result = divide(a, b);
3  // `result` type is: Number
4  print(c + 1);
5} catch {
6  // handle error
7}

Example in Ponylang:

1let result =
2  try
3    USize.max_value().div_partial(0)?
4  else
5    // handle error
6  end

For get item (from array at index) example in Python:

1from array import *
2myArray = array('i', [10,20,30,40,50])
3print (myArray[10])
4# IndexError: array index out of range

Undefined

Type signature: divide :: (Number, Number) -> Number | Undefined

Return special value for undefined behavior.

1result = divide(a, b);
2// `result` type is: Number | Undefined
3if (result == Undefined) {
4  // handle error
5} else {
6  // Now we know that `result` type is: Number
7  print(c + 1);
8}

For division, it can be NaN (not a number) or Infinity. From language PoV, they can be considered as numbers, but from math PoV, they are not.

Example in Ponylang (it returns tuple [Number, Boolean] instead of Number | Undefined):

1let result =
2  match USize.max_value().divc(0)
3  | (_, true) =>
4    /* handle error */
5  | (let temp: USize, false) =>
6    temp + 1
7  end

For get item (from array at index) it can be undefined or null. Example in JavaScript:

1let myArray = [10, 20, 30, 40, 50];
2myArray[10]; // undefined

Monad

Type signature: divide :: (Number, Number) -> Either<Error, Number>

We can use Either monad for the division.

 1result = divide(a, b);
 2// `result` type is: Either<Error, Number>
 3result.bimap(
 4  () => {
 5    /* handle error */
 6  },
 7  (temp) => { // `temp` type is Number
 8    print(temp + 1); 
 9  }
10);

We can use Maybe monad for “get item”. Example in Elm:

1myArray = Array.fromList [10,20,30,40,50]
2Array.get 10 myArray -- Never

Dependent types

Type signature: divide :: (Number, NumberExceptZero) -> Number

We can define more precise types of functions. For example, allow only non-zero numbers as a second parameter for the division.

1// `b` type is Number
2if (b == 0) {
3  /* handle error */
4} else {
5  // `b` type is Number except 0
6  result = divide(a, b);
7  print(result + 1);
8}

Pay attention: error handling is done before division - to prove to type checker that b is not zero.

Comparison table

Note: one more way to handle division is 1/0=0

Thoughts

• If an exception is used to compensate for undefined behavior of partial function it can be represented with types instead
• If the given exception is a type error or not depends on how types defined