### 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.