James Earl Douglas
October 29, 2021
Linear types ensure that values are used exactly once.
Types make illegal states unrepresentable. -- Yaron Minsky
Linear types ensure that values are used exactly once.
What does "used" mean?
This definition of linear types is most like WikiWikiWeb's definition.
... linear objects' reference count is always exactly 1.
Other definitions, such as Linear Haskell, are rather more sophisticated.
linearity is a property of function arrows, not of types
(f x)
is "consumed" exactly once, then
x
is consumed exactly oncef
can only be called onceWe 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.
def concat[A: Monoid](x: A with Linear, y: A with Linear): A =
implicitly[Monoid[A]].concat(x, x)
val x = List(1, 2, 3).asInstanceOf[List[Int] with Linear]
val y = List(4, 5, 6).asInstanceOf[List[Int] with Linear]
val z = concat[List[Int]](x, y)
The Linear
trait comes from linear-scala.
def concat[A: Monoid](x: A with Linear, y: A with Linear): A =
// ^ error: [LinearTypes] y is never used
implicitly[Monoid[A]].concat(x, x)
// ^ ^ error: [LinearTypes] x is used 2 times
val x = List(1, 2, 3).asInstanceOf[List[Int] with Linear]
val y = List(4, 5, 6).asInstanceOf[List[Int] with Linear]
val z = concat[List[Int]](x, y)
For more examples, see input/src/main/scala/fix/ in linear-scala.
Linear types ensure that values are used exactly once.
This can help us write code that: