source-academy/js-slang

Tighten type checking of lists and arrays in Source Typed

Closed this issue · 1 comments

Currently, in Source Typed, the following code produces no type errors:

const xs: List<number> = list(1, 2, "a");
const arr: number[] = [1, 2, "a"];

This occurs because the types of the above declared list and array are treated as List<1 | 2 | "a"> and (1 | 2 || "a")[] respectively, which have a non-zero intersection with List<number> and number[], therefore no type clashes are found as per success typing.

However, it is possible to tighten the types here such that type clashes can still be detected even with success typing. This can be done by making the following modifications:

  • For lists, during typechecking, expand List<T> to Pair<T, List<T>>. This way, instead of checking the types of the entire list, the types of the list elements are checked one by one, which will result in type errors being identified for the above example when typechecking "a" against number.
  • For arrays, support the notion of literal array types. Using the above code as an example, if we treat the array [1, 2, "a"] to be of literal array type [1, 2, "a"], a type error will be thrown as there is no intersection between the literal array type [1, 2, "a"] and number[].

To be truly consistent with success typing, we have decided not to proceed in this direction.

const xs: List<number> = list(1, 2, "a");
const arr: number[] = [1, 2, "a"];

Hence, the code above should not be producing a type error as there is a non-zero intersection between List<1 | 2 | "a"> and List<number>, and between (1 | 2 || "a")[] and number[].