James Earl Douglas
August 29, 2021
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)
Enforcing single-usage can prevent certain kinds of runtime errors.
for {
x <- Some(6)
y <- Some(7)
x <- Some(8)
} yield x * y
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
?
8*7
, but is it meant to produce 6*7
?
x
bindings be deleted?
How can we catch this shadowing bug at compile time?
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.
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
Linear types ensure that values are used exactly once.
What does "used" mean?
For our purposes, "used" simply means "dereferenced".
val foo = "foo"
println(foo) // first dereference
println(foo) // second dereference
Other definitions, such as Linear Haskell, are more sophisticated.
f :: A -o B
(f x)
is "consumed" exactly once, then x
is consumed exactly once
f
can only be called once
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.
For examples, see input/src/main/scala/fix/ in linear-scala.
Linear types can help us write code with fewer bugs.