Simon Peyton Jones - Linear Haskell: practical linearity in a higher-order polymorphic language

Curry On! · 18K views · 2018 · 1:03:34

Open on YouTube

Programming language designFunctional programmingtalk

Why Hacker News recommends it

HN recommends it as a clear introduction to linear types in GHC from the language's lead designer.

What it is

Simon Peyton Jones presents linear types for Haskell, showing how practical linearity can fit into a higher-order polymorphic language. The talk covers motivations such as resource handling and relates the ideas to Rust.

Recommended by 3 HN commenters across 3 different months, 2018 to 2020.

What Hacker News said

Recommends T-R · 2018-10 · on “Rust RAII is better than the Haskell bracket pattern”

Something to keep in mind - linear types are on their way[1], with exactly this usecase in mind. Simon Peyton Jones gave an excellent presentation on the topic[2], briefly discussing exceptions, as well as giving a mention to ResourceT and the phantom type solution in the article (described as channel-passing). [1] [LINK] [2] [this video]

Recommends throwaway17_17 · 2020-03 · on “Programming Models for Distributed Computation”

Session Types, AFAIU are a specific implementation of a linear logic in some type system and I am not all too familiar with them in practice. However, I would like to think I am well versed in Linear Logic and Substructural Type Theory. I think the works by Wadler are a good place to start, in particular is a sort of review paper, based in intuitionistic logic (which he also covers in said paper), on linear logic. It’s called ‘A Taste of Linear Logic’ (I actually have the paper open in Safari on my iPhone as I type this) and it is written as a sort of primer on the area. Wadler’s bibliographies on the works contained in the pages you linked are a good source as well. If you are at all coming

Recommends pyrale · 2020-09 · on “Haskell GHC 9.0.1-alpha”

SPJ usually makes great introductions about new things being introduced to GHC. Here's one about linear types: [this video] > How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc. In my own experience, you just practice, and munch new knowledge bits by bits. The crucial point here is that you don't need to know _all_ of haskell to be productive using it. So you learn the basics, start using monads without understanding the Monad abstraction (it's really not something you need to understand to use), and after a while it just clicks. And once you're confortable with th

Cites icc97 · 2018-09 · on “Ask HN: What topics/subjects are worth learning for a new software engineer?”

My personal opinion but this is purely because I enjoy it the most is functional programming. So much of the positive changes I've seen of late come through functional programming. For example: * ReasonML - this is what the founder of React is working on now. The ReasonML claims itself to be JavaScript 2030 (I see it as JavaScript + TypeScript + Immutable.JS + Redux). This contains a lot of the concepts from JavaScript so is a reasonable step to make * If ReasonML isn't too scary it leads you down a path to OCaml, F# and Elm * Rust (not strictly a functional programming language, but is ridiculously fast and contains well implemented Linear Types that makes Haskell's Simon Peyton-Jones jealo

Cites mauricioc · 2019-11 · on “Unsoundness in Pin”

Simon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung and others in the RustBelt project [1] did amazing work in formalizing Rust's safety guarantees, showing that Peyton Jones' guess was not accurate. There is nothing wrong about having bugs, of course, but the reaction to the bug in this thread shows that mathematical correctness is not as universally valued as I thought it would be. I agree with the sentiment that this is a bigger issue that shouldn't be discussed in a technical thread about a specific bug. However, after reading this, it is unclear to me whether mathematical correctnes

Cites T-R · 2020-09 · on “Haskell GHC 9.0.1-alpha”

My understanding is that the current implementation is only groundwork for possible future performance benefits, since there are no changes to the runtime system or garbage collector, and that their current intended use is mostly for allowing library authors to encode safe session/resource handling in the type system. So, new libraries can make it a type error to fail to properly close a connection or release a shared resource. Simon Peyton Jones talk: [this video]