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.