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

Remove untested typeclass elaboration #2434

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from

Conversation

facundominguez
Copy link
Collaborator

No description provided.

@facundominguez facundominguez force-pushed the fd/typeclass-elaboration branch from eeb9605 to da21f9a Compare November 11, 2024 18:44
@facundominguez
Copy link
Collaborator Author

facundominguez commented Nov 11, 2024

@ranjitjhala, @nikivazou, there is no test depending on the code in Bare.Elaborate which this PR is removing.

Section 3.2 of Verifying Replicated Data Types with Typeclass Refinements
in Liquid Haskell
seems to be explaining that such code is needed to introduce dictionaries in the predicates of refinement types.

Do you have any tests that rehearse this code? My first attempt to produce a test faced a crash.

@ranjitjhala
Copy link
Member

@nikivazou -- can you help with this? I am unfamiliar with the code? Is it "dead" code or no?

@ranjitjhala
Copy link
Member

I agree with @facundominguez btw that we should either add tests that exercise this functionality, or, if there is no such code because the type-class stuff has not been kept compatible, then we should just remove or comment it out...

@nikivazou
Copy link
Member

Correct! There are the test of the artifacts of the paper, I guess, not all of them are part of the test suite. Will try to find them and let you know.

@jprider63
Copy link
Contributor

Here are all the benchmarks from the paper. Probably the ones from liquid-base make the most sense to add to the test suite. It might even make sense to export the verified versions of typeclasses (like VSemigroup) in a library for others to use.

@nikivazou
Copy link
Member

Thanks!!!! I think it does not make sense to move all these in the test repo of Liquid Haskell..

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants