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?

Illuminating shadows

How can we catch this shadowing bug at compile time?

• Option 1: Prohibit shadowing
• 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
• Reading an input stream that has already been consumed
• Declaring a variable but forgetting to use it
• Shadowing a variable and using the wrong reference

For examples, see input/src/main/scala/fix/ in linear-scala.

Conclusion

Linear types can help us write code with fewer bugs.

Questions

References

• Linear Haskell: practical linearity in a higher-order polymorphic language, Simon Peyton Jones