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:

pub struct Peekable<I>
where
    I: [Iterator](https://doc.rust-lang.org/std/iter/trait.Iterator.html),{ /* private fields */ } {
    ..
    pub fn peek() -> Option<&<I as Iterator>::Item>
    ..
}

// values of type `Peekable<..> via:
trait Iterator {
  type Item;
  ..
  pub fn peekable(self) -> Peekable<Self>
}

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:

trait SomeTrait {
  method someTraitMethod()
}
method foo<T: SomeTrait>(arg: T) {
  arg.someTraitMethod();
}

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.