<p>Typescript's <a href="https://en.wikipedia.org/wiki/Structural_type_system" rel="nofollow noreferrer">structural type system</a> 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.</p>
<p>For example, the following snippet (<a href="https://www.typescriptlang.org/play?#code/C4TwDgpgBAYg9nKBeKBvAZggXFAzsAJwEsA7AcwF8AoUSWBAIQEMDk1M4d9jyAaKAEYsA-F0KlKVKugCuJAMbAicEoJYAKOAIBWOeHGYEAlDgBucIgBM0VKHajyV+KAjC4xPMmy3aAdENZhYSgAcgCQgG5be0cSXDgAGwhfBLgyTTg3IyjqaTlFZVUOTR09BBMocysbezUCEu1sqlzY5x82DGxQjhD+AJwAJgBmCijinyagA" rel="nofollow noreferrer">Playground Link</a>) compiles with no errors, but <code>oops</code> has type <code>string</code> at compile-time while its value at runtime will be a <code>number</code>:</p>
<pre class="lang-typescript prettyprint-override"><code>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);
</code></pre>
<p>The logic for this is as follows:</p>
<ul>
<li><code>{foo: string, bar: string}</code> is a subtype of <code>Foo</code> since it has all of the required properties.</li>
<li><code>Foo</code> has all of <code>FooBar</code>'s required properties, so a value of type <code>Foo</code> is assignable to <code>FooBar</code>.</li>
<li><code>FooBar</code>'s property <code>bar</code> is of type <code>string</code>, if it exists.</li>
</ul>
<p>The mistake is in step 2, where we suppose that a value of type <code>Foo</code> doesn't have any additional properties which might conflict with <code>FooBar</code>'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.</p>
<p>How can types with optional properties be made sound, while still keeping them useful?</p>

<types><static-typing><structural-types><soundness>
How can optional properties be made sound in a static structural type system?
CC BY-SA 4.0
2023-05-22T16:16:20.093Z
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.
mousetail 'he-him'
CC BY-SA 4.0
2023-05-22T16:17:03.847Z
Even if we considered different types separate "keys" effectively it would solve the issue for primitives but not objects
mousetail 'he-him'
CC BY-SA 4.0
2023-05-22T17:35:47.317Z
@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.
kaya3
<p>This is arguably a problem in your step <em>3</em>, with the dynamic semantics of the <code>??</code> operator, rather than step 2. There is no issue with assigning a value into a supertype.</p>
<p><strong>The <code>??</code> operator should confirm that the field in the dynamic object matches the locally-expected static type</strong>, not merely that it exists, and behave as though the field is absent otherwise. The soundness issue is that <code>??</code> is returning a value of the wrong type, not that the <code>bar</code> field is present dynamically.</p>
<p><code>bar</code> should not be accessible without confirming its presence with a matching type, so the same should happen for the <code>in</code> operator and any other way of narrowing the object type.</p>
<p>This is operating under the model that the optional property is an optional <em>property</em>: that this type is thus <code>{foo: string, bar: string} | {foo: string}</code>, which does not have a <code>bar</code> field: you <em>must</em> have a downcast to the two-field type to access it, and that cast can only be dynamically checked.</p>
<p>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.</p>
<hr />
<p>Of course, you <em>can</em> also reject the program at step 2, prohibiting the call to <code>bar</code> 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 <em>optional type</em>: <code>{foo: string, bar: string | undefined}</code>. In this case, <code>bar(obj);</code> is a static type error in a sound system, because the property does not exist on type <code>Foo</code>, and the program never gets to the point of dynamic values.</p>
<p>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.</p>

CC BY-SA 4.0
2023-05-23T01:27:13.317Z
2023-05-23T20:50:15.333Z
2023-05-23T20:50:15.333Z
Michael Homer
CC BY-SA 4.0
2023-05-23T01:31:30.267Z
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": https://coffeescript.org/#try:foo.bar%3F()
Bbrk24
CC BY-SA 4.0
2023-05-23T09:10:38.567Z
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.
kaya3
CC BY-SA 4.0
2023-05-23T09:28:26.587Z
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.
Michael Homer
CC BY-SA 4.0
2023-05-23T20:59:43.577Z
@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.
Michael Homer
# How can optional properties be made sound in a static structural type system?
Posted by: username_0 on 2023-05-22
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?
**Tags:** types static-typing structural-types soundness
> **Comments:**
> **username_1**: 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.  
> **username_1**: Even if we considered different types separate "keys" effectively it would solve the issue for primitives but not objects  
> **username_0**: @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.  
---
## 1 answers
### Answer by username_2 on 2023-05-23. Score: 5
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.
> **Comments:**
> **username_3** (2023-05-23): 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": https://coffeescript.org/#try:foo.bar%3F()  
> **username_0** (2023-05-23): 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.  
> **username_2** (2023-05-23): 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.  
> **username_2** (2023-05-23): @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.  
---
