You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Many languages provide the ability to put bounds on type parameters. For example, Java allows bounded type parameters, Rust allows bounding type parameters and lifetimes, and C# allows [constraints on type parameters]. When modeling standard libraries in such languages, types making use of such features are hard to model in Dafny.
It would be useful for interfacing with libraries in various target languages if Dafny had support for constraints on type parameters. It would also allow uses to be more precise in their type signatures, for example by specifying that a given type parameter needs to implement multiple traits (without needing to create a new trait definition combining this particular combination of traits).
Background and Motivation
As a motivating example, consider the Peekable trait from the Rust standard library:
Writing a Dafny binding to the Peekable/Iterator APIs is currently not feasible since the type parameter to Peekable cannot be expressed in Dafny.
Given that this is the prevalent abstraction pattern in Rust, used in places where object-oriented languages would often use subtyping / inheritance, I would expect this problem to occur with other commonplace Rust libraries as well.
Proposed Feature
Dafny could offer a similar feature and syntax as other languages. For example, whenever type parameters are specified, Dafny could allow the following:
Type-checking could follow the same implementation strategies as for Java, C#, or Rust. I'm not sure whether this feature would have non-trivial interactions with the verifier, given that it is purely a type system extension.
Alternatives
When writing code that interfaces with these parts of the Rust standard library, a user is instead forced to manually create monomorphized instances of Peekable instead. This creates a maintenance burden linear in the number of type parameters a type like Peekable is used with and requires error-prone copying and pasting of similar code. Additionally, one would have to redeclare all members of the trait for each monomorphized instance on the Dafny side.
Other solutions could include automatic translation of Dafny traits to bounded type parameters in Rust, but this does not address cases like the above where the type parameter cannot be specified at the Dafny level.
The text was updated successfully, but these errors were encountered:
Summary
Many languages provide the ability to put bounds on type parameters. For example, Java allows bounded type parameters, Rust allows bounding type parameters and lifetimes, and C# allows [constraints on type parameters]. When modeling standard libraries in such languages, types making use of such features are hard to model in Dafny.
It would be useful for interfacing with libraries in various target languages if Dafny had support for constraints on type parameters. It would also allow uses to be more precise in their type signatures, for example by specifying that a given type parameter needs to implement multiple traits (without needing to create a new trait definition combining this particular combination of traits).
Background and Motivation
As a motivating example, consider the
Peekable
trait from the Rust standard library:Writing a Dafny binding to the
Peekable
/Iterator
APIs is currently not feasible since the type parameter toPeekable
cannot be expressed in Dafny.Given that this is the prevalent abstraction pattern in Rust, used in places where object-oriented languages would often use subtyping / inheritance, I would expect this problem to occur with other commonplace Rust libraries as well.
Proposed Feature
Dafny could offer a similar feature and syntax as other languages. For example, whenever type parameters are specified, Dafny could allow the following:
Type-checking could follow the same implementation strategies as for Java, C#, or Rust. I'm not sure whether this feature would have non-trivial interactions with the verifier, given that it is purely a type system extension.
Alternatives
When writing code that interfaces with these parts of the Rust standard library, a user is instead forced to manually create monomorphized instances of
Peekable
instead. This creates a maintenance burden linear in the number of type parameters a type likePeekable
is used with and requires error-prone copying and pasting of similar code. Additionally, one would have to redeclare all members of the trait for each monomorphized instance on the Dafny side.Other solutions could include automatic translation of Dafny traits to bounded type parameters in Rust, but this does not address cases like the above where the type parameter cannot be specified at the Dafny level.
The text was updated successfully, but these errors were encountered: