Catching Resource Bugs at Compile Time!

For the next session, Olivier Lischer, a Master's student at OST in Rapperswil, will present "Linear Haskell - Practical Linearity in a Higher-Order Polymorphic Language". Linear Types: A type system paradigm that tracks resource usage (like file handles, memory pointers, etc) and rules out violations at compile time, already found in mainstream languages like Rust. Haskell: A strongly typed functional programming language used in high-assurance software. A priori, Haskell's type system said nothing about how many times a value is used. Linear types add exactly that: a function can require its argument to be consumed exactly once. This is enough to encode resource protocols in types, so using an array after it has been frozen, or a handle after it has been closed, becomes a type error instead of a runtime one. Why care? For PL and type-theory enthusiasts: this is Girard's linear logic, thirty years old, showing up in a compiler you already use. The interesting bit is the compromise: making linearity coexist with all the ordinary Haskell code that came before it is harder than the theory, and the design choices there are where the talk gets fun. For performance-minded programmers: linearity is how you get in-place mutation behind a pure interface. An array that is consumed exactly once can be updated destructively without anyone observing the difference, so you keep equational reasoning and drop the copy. This is a joint talk with HaskellerZ. The talk will be 45–60 minutes, followed by discussion and Q&A. No prior background in type systems is required; basic familiarity with functional programming will help.