10
$\begingroup$

Typescript's structural type system is known to be (intentionally) unsound, in the sense that the value of an expression at runtime is not always necessarily assignable to its type determined at compile-time.

For example, the following snippet (Playground Link) compiles with no errors, but oops has type string at compile-time while its value at runtime will be a number:

type Foo = {foo: string}
type FooBar = {foo: string, bar?: string}

function bar(obj: FooBar): void {
    const oops: string = obj.bar ?? 'bar';
    console.log(oops);
}

function foo(obj: Foo): void {
    bar(obj);
}

const obj = {foo: 'foo', bar: 23};
foo(obj);

The logic for this is as follows:

  • {foo: string, bar: string} is a subtype of Foo since it has all of the required properties.
  • Foo has all of FooBar's required properties, so a value of type Foo is assignable to FooBar.
  • FooBar's property bar is of type string, if it exists.

The mistake is in step 2, where we suppose that a value of type Foo doesn't have any additional properties which might conflict with FooBar's optional properties. However, this seems like an assumption we would want to be able to make in our type system, and not being able to make this assignment would be inconvenient.

How can types with optional properties be made sound, while still keeping them useful?

$\endgroup$
3
  • $\begingroup$ Optional types are not even necessary to create unsoundness, even just union types ca cause this, something like a: {} | {b: number} = {b: string} is possible with some intermediate steps. $\endgroup$
    – mousetail
    May 22, 2023 at 16:16
  • $\begingroup$ Even if we considered different types separate "keys" effectively it would solve the issue for primitives but not objects $\endgroup$
    – mousetail
    May 22, 2023 at 16:17
  • $\begingroup$ @mousetail That's true if the language allows undiscriminated unions, but in that case the unsoundness is clearly that 'b' in obj incorrectly narrows out the {} branch, when that branch is fully allowed to have a property named b. Undiscriminated unions and unsound property tests are a different can of worms; this unsoundness is caused purely by optional properties, which are a more desirable feature for a language to have than undiscriminated unions are. $\endgroup$
    – kaya3
    May 22, 2023 at 17:35

1 Answer 1

5
$\begingroup$

This is arguably a problem in your step 3, with the dynamic semantics of the ?? operator, rather than step 2. There is no issue with assigning a value into a supertype.

The ?? operator should confirm that the field in the dynamic object matches the locally-expected static type, not merely that it exists, and behave as though the field is absent otherwise. The soundness issue is that ?? is returning a value of the wrong type, not that the bar field is present dynamically.

bar should not be accessible without confirming its presence with a matching type, so the same should happen for the in operator and any other way of narrowing the object type.

This is operating under the model that the optional property is an optional property: that this type is thus {foo: string, bar: string} | {foo: string}, which does not have a bar field: you must have a downcast to the two-field type to access it, and that cast can only be dynamically checked.

Typescript is not able to do all this because it has to behave compatibly with the JavaScript nullish coalescing operator that is not type-aware, but that isn't in play for a language designed to have sound structurally-typed optional properties.


Of course, you can also reject the program at step 2, prohibiting the call to bar in the first place, and it will still be sound. This would be the approach if the optional property is actually a property of an optional type: {foo: string, bar: string | undefined}. In this case, bar(obj); is a static type error in a sound system, because the property does not exist on type Foo, and the program never gets to the point of dynamic values.

That does avoid changing the dynamic behaviour of type-inspection operations, and so would be more viable for a more-sound Typescript, only rejecting some more programs that would have worked. In a novel design, it's not clear that would ever be preferable.

$\endgroup$
4
  • $\begingroup$ As an example of this in practice, CoffeeScript's optional call operator doesn't just check that the property exists and is nonnull, it checks that its typeof is "function": coffeescript.org/#try:foo.bar%3F() $\endgroup$
    – Bbrk24
    May 23, 2023 at 1:31
  • $\begingroup$ I disagree. The same line without ?? ─ that is, const oops: string | undefined = obj.bar; would be equally unsound. Of course any static type system can be made sound by inserting runtime type checks where needed, but the question here is how to do it statically. Your proposal is to change the language to make the type checker's result correct, but I'm looking for a way to change the type checking rules to catch this error. $\endgroup$
    – kaya3
    May 23, 2023 at 9:10
  • 1
    $\begingroup$ Yes, const oops: string | undefined = obj.bar would just be a type error in a system that wanted soundness; {foo: string, bar?: string} is equivalent to {foo: string, bar: string} | {foo: string}, which does not have a bar field (no, it isn't in Typescript for the same reason, but it would be in a language that wanted soundness). If you want to access bar at all you need a dynamic cast, because you don't know if it's there or not, and that dynamic cast needs to make a runtime check. The purely-static solution is below the bar. $\endgroup$
    – Michael Homer
    May 23, 2023 at 9:28
  • $\begingroup$ @kaya3 I have edited the answer to be explicit about this, but: the model above the line is for sound treatment of an optional property (which may not be there, and so must be dynamically cast & checked - this is a downcast like from Object to String), and the one below the line is for sound treatment of a property of an optional type (whose value may not be there/holds an Option<string>). Those are the options for a sound structural model, which is what the question is about - Typescript conflates all these things, but you can't keep your unsound behaviour and have your sound system too. $\endgroup$
    – Michael Homer
    May 23, 2023 at 20:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .