Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Linearity, Uniqueness, Ownership: An Entente Co...

Linearity, Uniqueness, Ownership: An Entente Cordiale [POPL 2022 SRC]

Daniel Marshall

January 18, 2022
Tweet

Other Decks in Research

Transcript

  1. Some data is unrestricted. but… some data is resourceful. infinitely

    copiable arbitrarily discardable universally mutable 2/12
  2. Linear types are like cakes. You can only eat them

    once. You have to eat them. {-# LANGUAGE LinearTypes #-} desire : : Cake (Happy, Cake) desire cake = (eat cake, have cake) ⊸ 3/12
  3. Unique types are like coffee. A fresh coffee has just

    been poured. We can sip our coffee, but… then it is no longer fresh! share : : *Coffee - > (Awake, *Coffee) share coffee = (drink coffee, keep coffee) 4/12
  4. “But what’s the difference?” Linear types restrict a value from

    ever being duplicated (or discarded) in the future. Unique types guarantee that a value has never been duplicated in the past. 5/12
  5. “So can we use both?” Linear values as the base.

    Linear a Unique !a Cartesian *a borrowing dereliction Cartesian values under a comonadic ! modality. Unique values under an additional * modality. 6/12
  6. Unit laws and associativity hold! The ! modality acts as

    a relative monad over *. Γ ⊢ t : *A Γ ⊢ &t : !A borrow Γ1 ⊢ t1 : !A Γ2 , x : *A ⊢ t2 : !A Γ1 + Γ2 ⊢ copy t1 as x in t2 : !A copy Γ ⊢ *A Γ ⊢ !A (return) Γ1 ⊢ !A Γ2 , x : *A ⊢ !A Γ1 + Γ2 ⊢ !A (bind) 7/12
  7. “And is there an implementation?” • Already has a linear

    base. • Already represents ! as a coeffect (dual to effects). • Represent * as a third flavour of modality (called a guarantee). Yes - in Granule! sip : *Coffee - > (Awake, !Coffee) sip fresh = let !coffee = &fresh in (drink coffee, [keep coffee]) https://granule-project.github.io 8/12
  8. Time (ms) 0 175 350 525 700 Iterations 100 200

    300 400 500 Time (ms) 0 50 100 150 200 Iterations 100 200 300 400 500 Overall runtime Garbage collection overhead We evaluate our system using unique arrays. It’s safe to mutate these in place, so uniqueness gives us some performance benefits! 9/12
  9. So what about ownership? Ownership can be modelled via capabilities.

    Borrowing splits capabilities into fractions. x y x &mut y y &x 10/12
  10. So what about ownership? Linear types can be generalised to

    allow for quantitative restrictions. Unique types can be generalised to allow for fractional guarantees. !2 a - > a x a *1/2 a x *1/2 a < - > *a (similar to bounded linear logic) (similar to fractional permissions) 11/12
  11. @starsandspirals https://starsandspira.ls Thanks for watching! Some references: “Quantitative program reasoning

    with graded modal types” Orchard, Liepelt, Eades (2019) “Linear Haskell: Practical linearity in a higher-order polymorphic language” Bernardy, Boespflug, Newton, Jones, Spiwack (2018) “Making uniqueness typing less unique” de Vries, advised by Plasmeijer (PhD thesis) (2009) “Oxide: the essence of Rust” Weiss, Gierczak, Patterson, Ahmed (2021) Mutant Standard and Ferris the Rustacean emoji used under a Creative Commons BY-NC-SA 4.0 International license! 12/12