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

Typed Source: (Proposal) Unary + literal should be a literal type #1532

Closed RichDom2185 closed 7 months ago

RichDom2185 commented 9 months ago

Consider the following program:

const x: 2 = -4;

The program compiles successfully.

The unary operator - acts on the literal 4 to produce -4, but since this is typed as number, it raises no errors when trying to assign to symbol x of type 2 (due to success typing).

Proposal: Allow the unary operators to infer the type of its operand as a literal type.

RichDom2185 commented 9 months ago

Prof @martin-henz, can I get your thoughts on this?

RichDom2185 commented 9 months ago

Likewise for the binary string concatenation operator +:

image

Perhaps we could have literal types or even template literal types (in the case that one of the operands is of type string)?

RichDom2185 commented 9 months ago

And likewise for the boolean operators:

const t: true = true;
const f: false = false;
const bool1: true = !t; // !!
const bool2: false = f || f || t || f; // !!
martin-henz commented 9 months ago

I think you are confusing compile time (type-check time) with runtime. In general, the result of s1 + s2 will only be known at runtime, so the return type of the + operator at type-check time should be (string | number). Treating special cases as in the 'not actually hi' example above would be a hack. The question would arise how much effort does the type checker invest in order to "evaluate" expressions and figure out their literal type.

My hunch is that we should not go down that route. We should just treat the unary minus to have number as the return type, as far as the type checker is concerned. That will make things easy to explain.

const x: 2 = -4; // pass the type checker

should be a feature, not a bug.