Skip to content

Conversation

@seebees
Copy link
Contributor

@seebees seebees commented Nov 20, 2024

Dafny has optional parameters.

Smithy-Dafny uses this feature
to produce Dafny types
that default to := None.

However, the translated Dafny
does not support optional parameters.

This means that these optional parameters,
are not interoperable in target runtimes.

.NET already deferred type conversions
of wrapped resources to the target module.
But it assumed that Dafny was overly interoperable.

This change to .NET defers all type conversion
to the module that owns the type.
This brings .NET more in line with other runtimes.

This change is not completely backwards compatible.
There are a few edge cases with orphaned types
as well as already published versions.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@seebees seebees requested a review from a team as a code owner November 20, 2024 00:49
@josecorella josecorella force-pushed the seebees/net-type-conversion-encapsulation branch from 884b6bc to 34f5452 Compare January 31, 2025 18:57
seebees and others added 7 commits February 3, 2025 15:17
Dafny has optional parameters.

Smithy-Dafny uses this feature
to produce Dafny types
that default to `:= None`.

However, the translated Dafny
does *not* support optional parameters.

This means that these optional parameters,
are _not_ interoperable in target runtimes.

.NET already deferred type conversions
of wrapped resources to the target module.
But it assumed that Dafny was overly interoperable.

This change to .NET defers all type conversion
to the module that owns the type.
This brings .NET more in line with other runtimes.

This change is not completely backwards compatible.
There are a few edge cases with orphaned types
as well as already published versions.
@josecorella josecorella force-pushed the seebees/net-type-conversion-encapsulation branch from 756ce36 to 95adb6d Compare February 3, 2025 23:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants