August 29, 2021

# What are linear types?

Linear types ensure that values are "used" exactly once. More on this later.

``val x = 0``
``````val y = 1
println(y)``````
``````val z = 2
println(z)
println(z)``````

# Why are linear types interesting?

Enforcing single-usage can prevent certain kinds of runtime errors.

# Spot the bug

``````for {
x <- Some(6)
y <- Some(7)
x <- Some(8)
} yield x * y``````

# Which `x` is which?

``````for {
x <- Some(6) // x = 6
y <- Some(7) // y = 7
x <- Some(8) // x = 8
} yield x * y``````
• `x` is `8`, but is it meant to be `6`?
• This code produces `8*7`, but is it meant to produce `6*7`?
• Can one of these `x` bindings be deleted?

How can we catch this shadowing bug at compile time?

• Option 2: Require that all variables be used

# Make it linear

``````for {
x <- Some(6.asInstanceOf[Int with Linear])
y <- Some(7.asInstanceOf[Int with Linear])
x <- Some(8.asInstanceOf[Int with Linear])
} yield x * y``````

The `Linear` interface comes from linear-scala.

# Make it linear

``````for {
x <- Some(6.asInstanceOf[Int with Linear])
//^ error: [LinearTypes] x is never used
y <- Some(7.asInstanceOf[Int with Linear])
x <- Some(8.asInstanceOf[Int with Linear])
} yield x * y``````

# Defining linear types

Linear types ensure that values are used exactly once.

What does "used" mean?

# Linear types in linear-scala

For our purposes, "used" simply means "dereferenced".

``````val foo = "foo"
println(foo) // first dereference
println(foo) // second dereference``````

# Linear types in general

Other definitions, such as Linear Haskell, are more sophisticated.

``f :: A -o B``
• If `(f x)` is "consumed" exactly once, then `x` is consumed exactly once
• This does not mean that `f` can only be called once

# Implementing linear types in Scala

We can write custom linting rules with Scalafix to access to our code's AST through the Scalameta Trees API.

For implementation, see LinearTypes.scala in linear-scala.

# Common use cases

• Reading a file after it has been closed
• Updating a database after a transaction has been committed