Arnaud Spiwack (Tweag)
Date: Thursday, May 12 2022 – 11h00
Place: B013
Title: Linear Haskell
Since 2016, I’ve been leading the effort to supplement the
functional programming language Haskell with linear typing (in
the sense of linear logic). That is you can write a type of
functions which are allowed to use their arguments just once. The
first iteration of this was released as part of GHC 9.0.
This may seem like a curious property to require of a
function. Originally, linear logic was motivated by
proof-theoretic consideration. At first it appeared as a natural
decomposition of the coherence-space models of classical logic,
but it does have far reaching proof-theoretical
considerations. I’m one to take the connection between proof
theory and programming languages (the Curry-Howard
correspondence) quite seriously. Linear logic has almost
immediately been seen, from a programming language standpoint, as
giving a way to model resources in types. But what this
concretely means is not super clear. In this talk I will describe
the sort of practical benefits that we expect from linear types
in Haskell today. They are, in particular, related to Rust’s
ownership typing, though I don’t know whether I will have time to
explain this in detail. At any rate, I am not going to spoil the
entire talk here. I’d do a bad job of it in these handful of
lines, anyway.
