search

smithy-lang / smithy-dafny

Apache License 2.0
9 stars 8 forks source link

Support `@default` trait #544

Open texastony opened 2 weeks ago

texastony commented 2 weeks ago

Evolving Models

In theory, Smithy helps developers avoid Breaking changes.

It does this by publishing tooling and guides that dictate what changes are breaking vs those that are not.

In particular Update structures is of interest.

The following changes to structure shapes are backward-compatible: …

  1. Removing the required trait from a structure member and replacing it with the default trait (assuming the member was not marked with the clientOptional trait).

However, this is not possible for Smithy-Dafny consumers at this time, because Smithy-Dafny does not support the default trait.

Example case

In MPL#594, Crypto Tools removed the @required trait from a String, ddbTableName.

This passed all of the MPLs CI, but once Crypto Tools started testing against the DB-ESDK, Crypto Tools realized the Dafny type had subtly changed from string to Option<string>. See DB-ESDK#1313.

This is only test code, so Crypto Tools may not be blocked...

But Smithy cannot be fully utilized with out the @default trait.

texastony commented 2 weeks ago

In the case of this String, rather than just removing @required, Crypto Tools could replace @required with @default(""), and then let the business logic treat "" as None.

The business logic already is required to assert 3 <= |ddbTableName| <= 255, or something like that.

But the Dafny type would not change from string to Optional<string>.

seebees commented 2 weeks ago

This is likely a separate issue, but there is a similar complexity around @extendable rescues. How can you add new operations to such a shape?

robin-aws commented 1 week ago

@seebees Excellent point but definitely a separate issue - @default is an existing Smithy trait that isn't designed to be used for resources or operations in the way you might be thinking. See https://github.com/smithy-lang/smithy-dafny/issues/558

I also cut https://github.com/smithy-lang/smithy-dafny/issues/557 as the breakage described in the example was preventable.

texastony commented 1 week ago

Well, the breakage would have preventable IF and ONLY IF Smithy-Dafny respects @default...

robin-aws commented 1 week ago

The breakage would have been caught at the time of removing @required if smithy diff was run on the change.

Still being able to make the change anyway by also adding @default depends on smithy-dafny supporting it, true. But at least you would have known before changing MPL that you were going to break consumers.