u/Epistechnein r/functionalprogramming • Recommends
A Hitchhiker's Guide to Linearity by Daniel Marshall | Lambda Days 2023
0:00 / 0:00
#lineartypes#rustownership#haskell
A Hitchhiker's Guide to Linearity by Daniel Marshall | Lambda Days 2023
Code Sync
15K subscribers • 57 videos on Hallway
- Recommended by 2 people: 2 in engineering communities.
- Presented by Daniel Marshall
Intermediate. Assumes working knowledge.
1.2K views3 years ago2 recommendations
Programming languagesComputer scienceLanguage design and type systemsFunctional programming
Daniel Marshall explores the design space of linear, uniqueness, and quantitative types across languages like Haskell, Idris, and Rust.
Ever since Girard came up with linear logic back in the 1980s, computer scientists have been trying to figure out how to bring the idea of linearity into the realm of programming languages in order to demonstrate benefits in the real world. Nowadays, there are enough languages starting to take inspiration from linear logic to make your head spin; whether it's linear types in Haskell, uniqueness types in Clean, quantitative types in Idris, or the ownership system in Rust, there seems to be a different approach for everyone - but which is right for you? In this talk, we'll take a whirlwind tour through the design space. I'll explain the strengths and weaknesses of each of these ideas and show you how mixing and matching them can help to improve both safety and performance when working with resources such as file handles, mutable arrays, and communication channels, taking lessons from my ongoing work towards unifying these various concepts in our very own research language, Granule. Let's stay in touch! twitter.com/LambdaDaysWhy it's here
2 people recommend thisWhat people say. Recommended as a clear and comprehensive overview of linear types and ownership models in modern programming languages.
u/mttdin r/ProgrammingLanguages • Recommends
A Hitchhiker's Guide to Linearity by Daniel Marshall | Lambda Days 2023
u/mttdin r/ProgrammingLanguages • Mentions
On “Higher RAII, and the Seven Arcane Uses of Linear Types”
The Granule Language is also worth a look, https://granule-project.github.io/granule.html
I really liked the talk by Daniel Marshall (one of the authors), "A Hitchhiker's Guide to Linearity" (Lambda Days 2023), link to this video with the following distinction and examples:
- Linear types - restrict a value from ever being duplicated (or discarded) in the _future_ (e.g., file handles always closed after opening)
- Unique types - guarantee that a value has never been duplicated in the _past_ (e.g., unique arrays can be mutated in place without having to worry about aliasing/shared mutable state, as we're guaranteed there's none)
There's also two papers on the project:
- "Linearity and Uniqueness: An…
u/WittyStick0in r/ProgrammingLanguages • Mentions
On “Not quite an affine type system”
The Granule developers are adding fractional guarantees to allow multiple references to mutable values where the ownership is split between references. Possessing part of a reference allows you to read, but you need full ownership to mutate. It's similar to reference counting.
Discussed briefly in link to this video
u/WittyStickin r/ProgrammingLanguages • Mentions
On “Implementation of Uniqueness Types (= Smart Pointer?)”
> This is precisely why I find it difficult to see Uniqueness Types as anything other than a more restrictive form of linear types.
Unique types are more similar to affine types, because they can be ignored, whereas linearity requires that the reference be consumed before losing scope.
The main difference as I see it between unique and affine is that uniqueness implies that there is a unique reference to a unique value, whereas affinity only requires that the reference itself is unique - the underlying value may be non-unique. You can have multiple affine/linear references to the same underlying value. It's not safe to mutate the value under an affine or linear reference and preserve refer…