James Earl Douglas

October 29, 2021

Linear types ensure that values are used exactly once.

Types make illegal states unrepresentable. -- Yaron Minsky

- No types
- Normal types
- Generic types
- Higher-kinded types
- Linear types

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

- If
`(f x)`

is "consumed" exactly once, then`x`

is consumed exactly once - This does not mean that
`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.

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

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

Linear types ensure that values are used exactly once.

This can help us write code that:

- Is more understandable
- Has fewer bugs

*Effective ML Revisited*, Yaron Minsky*Linear Haskell*(paper, talk), Simon Peyton Jones*Substructural type system*, Wikipedia*Theorems for free!*, Philip Wadler- linear-scala