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.

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