https://arxiv.org/abs/2310.18166

Skip to main content
Cornell University
We gratefully acknowledge support from the Simons Foundation, member
institutions, and all contributors. Donate
 
arxiv logo > cs > arXiv:2310.18166
[                    ]

Help | Advanced Search

[All fields        ]
Search
arXiv logo
Cornell University Logo
[                    ] GO
quick links

  * Login
  * Help Pages
  * About

Computer Science > Programming Languages

arXiv:2310.18166 (cs)
[Submitted on 27 Oct 2023 (v1), last revised 15 Feb 2024 (this
version, v2)]

Title:Functional Ownership through Fractional Uniqueness

Authors:Daniel Marshall (University of Kent), Dominic Orchard
(University of Kent and University of Cambridge)
Download a PDF of the paper titled Functional Ownership through
Fractional Uniqueness, by Daniel Marshall (University of Kent) and 1
other authors
Download PDF

    Abstract:Ownership and borrowing systems, designed to enforce
    safe memory management without the need for garbage collection,
    have been brought to the fore by the Rust programming language.
    Rust also aims to bring some guarantees offered by functional
    programming into the realm of performant systems code, but the
    type system is largely separate from the ownership model, with
    type and borrow checking happening in separate compilation
    phases. Recent models such as RustBelt and Oxide aim to formalise
    Rust in depth, but there is less focus on integrating the basic
    ideas into more traditional type systems. An approach designed to
    expose an essential core for ownership and borrowing would open
    the door for functional languages to borrow concepts found in
    Rust and other ownership frameworks, so that more programmers can
    enjoy their benefits.
    One strategy for managing memory in a functional setting is
    through uniqueness types, but these offer a coarse-grained view:
    either a value has exactly one reference, and can be mutated
    safely, or it cannot, since other references may exist. Recent
    work demonstrates that linear and uniqueness types can be
    combined in a single system to offer restrictions on program
    behaviour and guarantees about memory usage. We develop this
    connection further, showing that just as graded type systems like
    those of Granule and Idris generalise linearity, Rust's ownership
    model arises as a graded generalisation of uniqueness. We combine
    fractional permissions with grading to give the first account of
    ownership and borrowing that smoothly integrates into a standard
    type system alongside linearity and graded types, and extend
    Granule accordingly with these ideas.

Comments: 27 pages + references. In submission (minor revision)
Subjects: Programming Languages (cs.PL)
Cite as:  arXiv:2310.18166 [cs.PL]
          (or arXiv:2310.18166v2 [cs.PL] for this version)
          https://doi.org/10.48550/arXiv.2310.18166
          Focus to learn more
          arXiv-issued DOI via DataCite

Submission history

From: Daniel Marshall [view email]
[v1] Fri, 27 Oct 2023 14:22:00 UTC (70 KB)
[v2] Thu, 15 Feb 2024 11:10:11 UTC (77 KB)
Full-text links:

Access Paper:

    Download a PDF of the paper titled Functional Ownership through
    Fractional Uniqueness, by Daniel Marshall (University of Kent)
    and 1 other authors
  * Download PDF
  * TeX Source
  * Other Formats

license icon view license
Current browse context:
cs.PL
< prev   |   next >
new | recent | 2310
Change to browse by:
cs

References & Citations

  * NASA ADS
  * Google Scholar
  * Semantic Scholar

a export BibTeX citation Loading...

BibTeX formatted citation

x
[loading...          ]
Data provided by:

Bookmark

BibSonomy logo Reddit logo
(*) Bibliographic Tools

Bibliographic and Citation Tools

[ ] Bibliographic Explorer Toggle
Bibliographic Explorer (What is the Explorer?)
[ ] Litmaps Toggle
Litmaps (What is Litmaps?)
[ ] scite.ai Toggle
scite Smart Citations (What are Smart Citations?)
( ) Code, Data, Media

Code, Data and Media Associated with this Article

[ ] Links to Code Toggle
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
[ ] DagsHub Toggle
DagsHub (What is DagsHub?)
[ ] GotitPub Toggle
Gotit.pub (What is GotitPub?)
[ ] Links to Code Toggle
Papers with Code (What is Papers with Code?)
[ ] ScienceCast Toggle
ScienceCast (What is ScienceCast?)
( ) Demos

Demos

[ ] Replicate Toggle
Replicate (What is Replicate?)
[ ] Spaces Toggle
Hugging Face Spaces (What is Spaces?)
[ ] Spaces Toggle
TXYZ.AI (What is TXYZ.AI?)
( ) Related Papers

Recommenders and Search Tools

[ ] Link to Influence Flower
Influence Flower (What are Influence Flowers?)
[ ] Connected Papers Toggle
Connected Papers (What is Connected Papers?)
[ ] Core recommender toggle
CORE Recommender (What is CORE?)

  * Author
  * Venue
  * Institution
  * Topic

( ) About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and
share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have
embraced and accepted our values of openness, community, excellence,
and user data privacy. arXiv is committed to these values and only
works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community?
Learn more about arXivLabs.

Which authors of this paper are endorsers? | Disable MathJax (What is
MathJax?)

  * About
  * Help

  * Click here to contact arXiv Contact
  * Click here to subscribe Subscribe

  * Copyright
  * Privacy Policy

  * Web Accessibility Assistance
  * arXiv Operational Status
    Get status notifications via email or slack