dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.87k stars 256 forks source link

Feature Request: Support trait types as a type parameter #599

Open acioc opened 4 years ago

acioc commented 4 years ago

Currently, we have a custom datatype MyDataType<T> = SomeValue(value: T) | NoValue(msg: string)

I wanted to have a custom trait, like

  trait {:extern "MyTrait"} MyTrait {
    method {:extern "SomeMethod"} SomeMethod()
  }

Essentially, we can implement MyTrait multiple ways and allow MyDataType to take in any of them (like we would with an interface in other languages). Although VSCode codes not (currently) show any errors, when compiling I get error : compilation does not support trait types as a type parameter; consider introducing a ghost

I was hoping this functionality could be supported, so we don't need to create custom datatype MyDataTypeForMyTrait<T> = SomeValue(value: MyTrait) | NoValue(msg: string) For every custom trait we create

seebees commented 2 years ago

@robin-aws I think that this is closed by #1499?