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

Fractional permissions for mutable and immutable borrowing #229

Merged
merged 84 commits into from
Nov 22, 2024
Merged

Conversation

starsandspirals
Copy link
Collaborator

@starsandspirals starsandspirals commented Nov 9, 2023

Introduces the extensions from the fractional uniqueness paper into Granule. Currently includes:

  • The additional 'borrow' modality, graded by a permission
  • Fractional grades as one instance of permissions, with algebraic operations and SMT constraints
  • withBorrow, split, join, push, pull primitives for mutable and immutable borrows, as in the paper
  • Well-typed interface for polymorphic references

Remaining tasks before this can be merged:

  • Existentially typed identifiers for arrays and references
  • Runtime behaviour for references (should be represented via Haskell IORefs managed via unsafePerformIO as with mutable arrays, pointing to Granule AST values)
  • Star alias for a 'unique' permission, additional to fractions
  • Derivable push and pull for arbitrary data types (let's call this a stretch goal, but it would be great to get there, and we do have an example based on this in the paper - can follow exactly the same schema as deriving for the box modality)
  • More descriptive error messages when working with borrows/fractions (minor)
  • More practical examples using arrays and references (minor)

@buggymcbugfix buggymcbugfix changed the base branch from dev-minor to main May 3, 2024 08:04
@dorchard
Copy link
Member

dorchard commented May 8, 2024

@starsandspirals - what's the status of this? I think it's pretty much ready to merge?

@dorchard
Copy link
Member

Bump on @starsandspirals - I believe we can merge this right?

@dorchard
Copy link
Member

I resolved the conflicts.

@dorchard dorchard marked this pull request as ready for review November 21, 2024 12:35
@dorchard dorchard merged commit 2a2e347 into main Nov 22, 2024
1 check failed
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.

3 participants