October 29, 2021

# Bottom line up front

Linear types ensure that values are used exactly once.

# Types are restrictive

Types make illegal states unrepresentable. -- Yaron Minsky

# A progression of type strength

1. No types
2. Normal types
3. Generic types
4. Higher-kinded types
5. Linear types

# No types

``function foo(x, y) { ... }``

# Normal types

``def foo(x: Int, y: Int): Int = ...``

ðŸ’ª

# Generic types

``def foo[A](x: A, y: A): A = ...``

ðŸ’ª ðŸ’ª

# Higher-kinded types

``def foo[A: Monoid](x: A, y: A): A = ...``

ðŸ’ª ðŸ’ª ðŸ’ª

# Linear types

``def foo[A: Monoid](x: A with Linear, y: A with Linear): A = ...``

ðŸ’ª ðŸ’ª ðŸ’ª ðŸ’ª

# Defining linear types

Linear types ensure that values are used exactly once.

What does "used" mean?

# Using values

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

# Linear types in general

This definition of linear types is most like WikiWikiWeb's definition.

... linear objects' reference count is always exactly 1.

# Linear types in Linear Haskell

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

linearity is a property of function arrows, not of types

# Linear types in Linear Haskell

``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.

# Spot the bug

``````def concat[A: Monoid](x: A, y: A): A =
implicitly[Monoid[A]].concat(x, x)

val x = List(1, 2, 3)
val y = List(4, 5, 6)
val z = concat(x, y)``````

# Make it linear

``````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.

# Make it linear

``````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)``````

# Make it right

``````def concat[A: Monoid](x: A with Linear, y: A with Linear): A =
implicitly[Monoid[A]].concat(x, y)

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)``````

# Spot the bug

``````val x = 6

def foo() = {
val x = 8
val y = 7
x * y
}``````

# Make it linear

``````val x = 6.asInstanceOf[Int with Linear]

def foo() = {
val x = 8.asInstanceOf[Int with Linear]
val y = 7.asInstanceOf[Int with Linear]
x * y
}``````

# Make it linear

``````val x = 6.asInstanceOf[Int with Linear]
// ^ error: [LinearTypes] x is never used

def foo() = {
val x = 8.asInstanceOf[Int with Linear]
val y = 7.asInstanceOf[Int with Linear]
x * y
}``````

# Make it right

``````val x = 6.asInstanceOf[Int with Linear]

def foo() = {
val y = 7.asInstanceOf[Int with Linear]
x * y
}``````

# Spot the bug

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

# 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``````

# 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``````

# Make it right

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

# Spot the bug

``````def read(s: Source): String =
try {
s.mkString
} finally {
s.close()
}

val s: Source =
Source.fromFile("/etc/passwd")

# Spot the bug

``````def read(s: Source): String =
try {
s.mkString
} finally {
s.close()
}

val s: Source =
Source.fromFile("/etc/passwd")

# Make it linear

``````def read(s: Source): String =
try {
s.mkString
} finally {
s.close()
}

val s: Source with Linear =
Source
.fromFile("/etc/passwd")
.asInstanceOf[Source with Linear]

# Make it linear

``````def read(s: Source): String =
try {
s.mkString
} finally {
s.close()
}

val s: Source with Linear =
Source
.fromFile("/etc/passwd")
.asInstanceOf[Source with Linear]

//           ^ error: [LinearTypes] s is used 2 times
//           ^ error: [LinearTypes] s is used 2 times``````

# Make it right

``````def read(s: Source): String =
try {
s.mkString
} finally {
s.close()
}

val s: Source with Linear =
Source
.fromFile("/etc/passwd")
.asInstanceOf[Source with Linear]

println(x)
println(x)``````

# Other use cases

• Ensure that a db queries aren't run after commit/rollback
• Ensure that a stream is fully consumed
• Ensure that a protocol is adhered to
• Debounce non-idempotent code
• Detect and prevent dead code

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

# Conclusion

Linear types ensure that values are used exactly once.

This can help us write code that:

• Is more understandable
• Has fewer bugs