Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
acioc opened this issue Apr 17, 2020 · 1 comment
Open

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

acioc opened this issue Apr 17, 2020 · 1 comment
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@acioc
Copy link
Collaborator

acioc commented Apr 17, 2020

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

@robin-aws robin-aws added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Jun 23, 2020
@acioc acioc added this to the Dafny 3.0 milestone Jul 22, 2020
@davidcok davidcok modified the milestones: Dafny 3.0, Dafny 3.1 Dec 23, 2020
@atomb atomb removed this from the Dafny 3.1 milestone Apr 21, 2022
@seebees
Copy link

seebees commented May 22, 2022

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Development

No branches or pull requests

6 participants