source-academy / js-slang

Implementations of sublanguages of JavaScript, TypeScript, Scheme and Python
https://source-academy.github.io/source/
Apache License 2.0
70 stars 104 forks source link

Tighten type checking of lists and arrays in Source Typed #1488

Closed zhaojj2209 closed 7 months ago

zhaojj2209 commented 1 year ago

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:

Zenkoh1 commented 7 months ago

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[].