Linear types allow expressing resource usage in the type system. They can, for example, ensure that an opened file handle must be closed or that an array can be updated in-place without affecting the values of other variables. Rust achieves similar ends using borrowing, which allows many programs to be expressed more conveniently. The paper below proposes an approach to get (some of) the convenience of borrowing, while being simpler and supporting a translation to “normal” linear types.

In your seminar paper, you will explain linear typing, the linear lambda calculus, and the approach to borrowing described in the paper. You will also illustrate the difference between linear typing and borriwng with self-written example programs in Linear Haskell and Rust.

Links