u/AnteaterofPowerin r/ProgrammingLanguages • Recommends
ATS: Why Linear Types are the Future of Systems Programming
0:00 / 0:00
#ats#lineartypes#dependenttypes
ATS: Why Linear Types are the Future of Systems Programming
Berlin Functional Programming Group
2K subscribers • 9 videos on Hallway
- Recommended by 2 people: 1 on Lobsters and 1 in engineering communities.
- Presented by Aditya Siram
- Linked in the descriptiondeech/FPBerlinATSTalk
- An opinion. It argues one side of a question engineers disagree on.
Advanced. Deep dive for people who know the field.
11K views5 years ago2 recommendations
Programming languagesSystems programmingLanguage design and type systemsMemory management
Aditya Siram explores how the ATS programming language uses linear and dependent types for safe, low-level systems programming.
With Aditya "Deech" Siram! This talk will explore why ATS, a linearly typed ML for systems programming, should be the inspiration for the next generation of systems programming languages. It will cover: - Using linear types for completely type safe C level control over memory manipulation and allocation. - Interleaving theorem proving and dependent types to emulate Rust-like mutability guarantees and more! - How linear types allow seamlessly mixing garbage-collected code with low-level pointer manipulation. - How ATS's new streaming primitive allows us to write higher order functional programs and precisely reason about in-the-moment resource usage for highly predictable but fast servers. - And maybe more depending on time and interest! Aditya is currently a Haskell programmer working on privacy software at LeapYear (leapyear.io). In his spare time, he has a strong interest in the intersection of functional programming, programming environments, tooling and developer experience, and high-performance, statically-verified software. Slides for this talk: github.com/deech/FPBerlinATSTalk/blob/master/Talk.pdf This virtual talk was brought to you by the Berlin Functional Programming Group. Join us on Meetup: meetup.com/Berlin-Functional-Programming-Group/ Follow us on Twitter: twitter.com/BerlinFPGroup Buy a T-shirt: teespring.com/berlin-fp-group Support us on Patreon: patreon.com/bfpgWhy it's here
2 people recommend thisWhat people say. Recommended as a compelling argument for linear types in systems programming.
Moments people linked to
januson Lobsters • Recommends
ATS or Why Linear Types are the Future of Systems Programming
u/FunctionalFox1312in r/ProgrammingLanguages • Mentions
On “What book(s) to read to understand Rust's type system?”
Rust uses linear types for its memory-safety type guarantees, to give you the language you need to start digging. Here's a good talk on them. Also go check out "Linear Lisp", an older book on the subject of adding linear types to a lisp, which Rust's original lead says didn't directly inspire him but probably figured in somewhere.
As for the general type system stuff... Rust is probably best understood as an ML-derivative with C syntax. You can take any book on OCaml to get an idea of how ML type systems generally work, and here's a PDF from Princeton on implementing an OCaml subset in OCaml. You can probably find a lot more in that vein, OCaml is a choice language for academic PL nerds…
u/cptwunderlichin r/ProgrammingLanguages • Mentions
On “"If you can compile it, there's probably no bugs" languages other than Haskell?”
I found Deech's introduction to ATS at Berlin FP group really interesting and eye opening. He basically says, that the concepts in the language are great, but the language itself is a messy research concoction.