# Linearity

## Table of contents

## Handling linearity

Most programming languages treat all values the same way, but FreeST is very different from them. FreeST has a `linear system`

which differentiates **linear** from **unrestricted** values and types. An unrestricted value is one that may be used **0 or more times** during the program’s execution(it’s what most programming languages have). A linear value or type is one that must be used **exactly once** during the program’s execution. If linear constraints are violated, the program will **not type check**, and therefore, will **not run**.

All constants are by default unrestricted values, so the following code is valid:

```
f : Int -> Int
f x = x + 1
main : ()
main =
let i = 5 in
f i ; -- both g and i are used once
f i ; -- both f and i are used twice
let j = 2 in
-- j is never used
()
```

Functions are the first construct programmers face that can also be linear. A **linear function** is simply a function that has to be used exactly once (following the linear constraint). Let us write a linear function `linIncrement`

that increments an integer by 1:

```
linIncrement : Int 1-> Int
linIncrement x = x + 1
```

If this function is part of your code, then you are obliged by linearity to use it. The following would not run:

```
linIncrement : Int 1-> Int
linIncrement x = x + 1
main : Int
main = 1
```

Fixing the above code is simple, just make sure you use `linIncrement`

exactly once, for example:

```
linIncrement : Int 1-> Int
linIncrement x = x + 1
main : Int
main = linIncrement 1
```

## Treading carefully with linear functions

Linear functions seem simple, however there is more to it than meets the eye. The type `Int 1-> Int`

describes a linear function that takes an integer and returns an integer, but what about type `Int 1-> Int -> Int`

? This type also describes a linear function, but with a twist: only the first part is linear (instead of the whole as before). If you partially apply a function of this type with a single integer, it will become an unrestricted function.

```
f : Int 1-> Int -> Int
f x y = x + y
main : Int
main =
let f' = f 1 in
f' 3 + f' 1 + f' 2
```

In the above case, after partially applying `f`

we get an unrestricted function `f'`

which we then use multiple times. A truly linear version of function `f`

would need to have type `Int 1-> Int 1-> Int`

.

Let us now analyse a similar in form, but quite different in behaviour, type `Int -> Int 1-> Int`

. This is more tricky than what we’ve seen until now. Let’s analyze it step by step, look at it as `Int -> (Int 1-> Int)`

. Now it’s clearer that it represents an **unrestricted** function that takes an integer and returns another **linear** function that takes an integer and returns an integer.

```
g : Int -> Int 1-> Int
g x y = x + y
main : Int
main =
let g1 = g 1 in
let g2 = g 2 in
g1 3 + g2 4
```

This time, function `g`

is used multiple times to create linear functions `g1`

and `g2`

, each of which is then used exactly once.

Functions `f`

and `g`

are fundamental to understand how functions deal with linearity and how us programmers should both write and use them. From here on out, there are many possible cases that combine both cases of `f`

and `g`

, but by breaking it down type by type as we did for `g`

, we can quickly understand any combination of linear and unrestricted functions.