Linearity, Uniqueness, Ownership: An Entente Cordiale
Substructural type systems, which restrict the use of weakening and contraction rules from intuitionistic logic, are growing in popularity because they allow for a resourceful interpretation of data which can be used to rule out software bugs. Substructurality is finally taking hold in practical programming: Haskell now has linear types based on Girard’s linear logic but integrated via graded function arrows, Clean has uniqueness types ensuring that values have at most a single reference, and Rust has an intricate ownership system guaranteeing memory safety. But despite this broad range of resourceful type systems, there has been comparatively little work on understanding their relative strengths and weaknesses. In our ESOP paper from 2022, we demonstrate how linear types and uniqueness types can be used within a single system in the setting of the Granule language to offer both restrictions on local program behaviour and guarantees about global memory usage. We then extend this framework further in work that will be presented later this week at OOPSLA, by showing that just like graded type systems as in Granule or Idris build upon linearity, Rust’s ownership model builds upon uniqueness. We develop an extended type system incorporating ownership and borrowing based on ideas from both fractional permissions and graded types, and implement this in Granule.
Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:30 | |||
16:00 30mTalk | The First Six Years in the Development of Polonius, an Improved Borrow Checker IWACO Amanda Stjerna Uppsala university File Attached | ||
16:30 30mTalk | Data-Race Safety for the Masses IWACO Holly Borla Apple, Inc, | ||
17:00 30mTalk | Linearity, Uniqueness, Ownership: An Entente Cordiale IWACO Danielle Marshall University of Glasgow |