# How to read code: the next generation

Reading type signatures will become the part of basic computer literacy curriculum taught in elementary schools.

While they taught you how Microsoft spreadsheets operated kids in future will learn some lambda calculus instead.

Types will be the standard user interfacing element to access computer systems. It will replace the buttons and text boxes of the present day and ordinary people will use them every day.

This article tells what these "types" are and gives a taste of how to read type signatures. Then I explain why I think this is useful and conclude with an example of reading code with types. I assume that you understand a bit of basic algebra.

## What kind of types?

You may have met types before, in mathematics. There are many types of numbers that have been labeled by their properties.

You may already know about natural numbers, integers and real numbers. You may have been told to calculate with fractions or with decimals. Types are already a widely taught subject, although their full utility has not yet been realised by laymen.

Lets take apart natural numbers by asking ourselves what is a natural number? We could start with the following definition:

- 0 is a natural number.
- If n is a natural number, then n+1 is a natural number.

Although it's an important question whether this is a good definition we won't discuss that for now. Instead, lets imagine a very stubborn person who tries to say that 5 is not a natural number. And lets say that he agrees on this definition, how would you prove him that 5 is a natural number?

You might throw 5 stones into a bucket, have him agree there is 5 stones in the bucket. Then you can say that number of stones in the bucket is a natural number.

If we were more formal about it, the proof would consist of steps that look like this:

- 0 is a natural number, therefore
- 0+1 is a natural number, therefore
- 0+1+1 is a natural number, therefore
- 0+1+1+1 is a natural number, therefore
- 0+1+1+1+1 is a natural number, therefore
- 0+1+1+1+1+1 is a natural number, and 0+1+1+1+1+1 is 5.

For anything to make sense after this point, you have to make an observation.

Isn't the number same as the proof? If we were to take a proof that states '3' is a number, it'd come with 3 steps. Proofs for natural numbers themselves form natural numbers.

This means that the proposition, "is a natural number",
can be treated as the type of natural numbers.
We could write `5 : Nat`

to make this explicit.

We've found a perspective on types that makes them logical propositions, and numbers themselves become proofs that prove they are what they are.

You might meet other people who would argue that 0 is not a natural number. To reason with them, you can tell their number system is shifted right by one in comparison to yours. They say 1 in the place of 0 when they define natural numbers (That's a joke. Don't do this as it would not be very diplomatic).

## There are more types

People have learned ways to define other types of numbers in formal logic. These definitions are useful, but they would not be in the first semester's material. However an important question is, are there other types than numbers?

If logical propositions are types, then we have other types than just numbers.

Lets start with ∧. This symbol is spelled out as "and"
and it combines two propositions together.
To prove `x∧y`

, you have to prove x and y.
A convenient way to write this down is to put comma and parentheses.
For example:

`(3, 5) : Nat ∧ Nat`

Would state that proof 3, and proof 5, forms a pair of natural numbers.

We also have "or", marked with ∨.
To prove this proposition,
you either have to prove left or right proposition.
The convention for this one may feel less natural
as it is customary to write `inl x`

for left proposition being proved,
and `inr y`

for right proposition being proved.

An example:

`inl 4 : Nat ∨ Real`

This states that the left proof 4, forms a natural number or a real number.

We need to introduce yet one logical proposition that is a type.
We call these types "functions" and mark them with a rightwards going arrow.
It is spelled out as "implies", and to prove `a → b`

,
you have to prove b while you assume a is already proven.
We mark the proof with a λ,
because lambda calculus is a proof system that only has this type.
A name is given, separated with a dot,
to stand as the name for the proof that was assumed.

An example:

`λx. x : Nat → Nat`

This states that given proof for Nat, you get a proof for Nat.

So far we've covered what is a proof for each structure, but there are also ways to take proofs to their constituents. For example, functions can be "applied" and it is denoted with space between terms.

The following three proofs would be the same.

`(λx. x) 2 : Nat`

`2 : Nat`

`(λx.λy. x) 2 3 : Nat`

The other propositions can be also taken apart to their constituents. ∧ can be projected to the first or second proof whereas ∨ can be case-matched. We can use the following notation for now:

`fst (x,y) = x`

`snd (x,y) = y`

`either f g (inl x) = f x`

`either f g (inr y) = g y`

If you find this difficult, focus on the propositions and try to verify you understand what they mean.

### "Magic trick" to get constituents of natural numbers

How to take a natural number to it's constituents? An one way to do so would be the Church encoding. These are called Church numerals.

`Nat ≡ ∀a. a → (a → a) → a`

This expression means that `Nat`

is named into some encoded type.
There's also a symbol ∀. It is spelled as "given any",
and when used this way stands "for any type".

Given any type `a`

, then given some proof for `a`

(zero),
and a proof for `a`

implying `a`

(successor function),
you get a proof for `a`

.
That's natural numbers through Church encoding.

In this way we loaned proofs and applicators of function type to get applicators for natural numbers.

## Utility of types

Learning to use types takes effort, but they relate to mathematics such as algebra that are already being taught in schools.

Types can be used to describe rules, such that it can be read by a computer while still being comprehensible. They can explain what you can get from a computer system, or what you have to supply to get results.

They make perfect user interfaces because computers can assist in their use and give predictions of what will happen for each command you can give. Likewise commands given through such interfaces can be recorded and repeated as needed.

Proofs are valid representations of programs. This means that types can be used when programming computers. If they were exposed as user interfaces, there would be a ladder for layman to gradually descent into doing real programming.

## Example of reading code from a simple program

The following program presents a playable tic-tac-toe board in a console. It has been written in Haskell while trying to keep the types simple. Therefore the types it presents are approximations of what they represent. I'm going to read through the types, then present the program.

The notation is slightly different from what was present earlier.
There are two colons instead of one colon,
and arrows are drawn as `->`

instead of `→`

.

Since the program doesn't encode what a valid play of tic-tac-toe is. We describe it shortly.

- Two players take turns placing pegs.
- First player to move places pegs labeled with crosses while second player to move places pegs labeled with circles.
- Player cannot place a peg over an existing peg.
- Player wins if he places his pegs, forming three of his marks in a horizontal, vertical or diagonal line.
- Peg must be placed on the board.
- If a player cannot do a move, it's a tie.

We could describe such valid play formally, in a bit similar manner how natural numbers were described. And peg could be an any element that can be used to describe the rules.

For now we settle to this though:

`type Run = [Peg]`

`type Peg = (Integer, Integer)`

`data Player = Cross | Circle`

The `Run`

is a sequence of pegs placed on the board,
it is separately checked that the newly placed peg
does not intersect existing pegs and that it is on the board.

Here's every type given in the program.

`whoseTurnItIs :: Run -> Player`

`priorMoves :: Run -> [Peg]`

`isValidMove :: Run -> Peg -> Bool`

`isWinningMove :: Run -> Peg -> Bool`

`line :: Integer -> Integer -> Peg -> Peg -> Bool`

`inBounds :: Peg -> Bool`

`bounds :: [Peg]`

`displayRun :: Run -> String`

`displayPeg :: Peg -> Run -> String`

`peg :: Peg -> Run -> Maybe Player`

`showPlayer :: Player -> String`

`main :: IO ()`

`play :: Run -> IO ()`

`check :: (a -> Bool) -> a -> Maybe a`

`charToPeg :: Char -> Maybe Peg`

Next we go through the judgements that describe how the playing board works.

`whoseTurnItIs :: Run -> Player`

`priorMoves :: Run -> [Peg]`

`isValidMove :: Run -> Peg -> Bool`

`isWinningMove :: Run -> Peg -> Bool`

`inBounds :: Peg -> Bool`

`bounds :: [Peg]`

`whoseTurnItIs`

provides whose turn it is next.
Note that it is applied to some `Run`

and gives you the `Player`

.

`priorMoves`

provides the sequence of moves that was made
by the next player to move.

`isValidMove`

tells whether the player can place a peg or not.
Likewise the `isWinningMove`

tells whether the player wins,
given a valid move that he did.

`inBounds`

describes whether the move is in boundaries.

`bounds`

enumerates every motion that is in boundaries and therefore could be valid.

There are some judgements that relate to how the game is implemented.

`line :: Integer -> Integer -> Peg -> Peg -> Bool`

`peg :: Peg -> Run -> Maybe Player`

`check :: (a -> Bool) -> a -> Maybe a`

`line`

checks whether two pegs end up on the same line.
The line is described with an implicit equation.

`peg`

takes a move and checks whether
it's been played by either player during the run.
It described which player played the run if it was played.

`check`

is an abstract function that is used to discard a result
if it doesn't check with a condition.
Notice how the `isValidMove`

, `isWinningMove`

, `inBounds`

,
fit together with this function.

There are some routines that provide a driver to play this game.

`main :: IO ()`

`play :: Run -> IO ()`

These judgements describe relatively little
of what goes inside `main`

and `play`

because Haskell does not
describe interactions with types.

Interactions could be described with types, but I would have to tell you a bit more about types before you could decipher them.

If those type did tell you what it does, it'd tell you that this program is an interactive console program.

Finally we have judgements that allow the game to be displayed in the console, and interpret the input as game movements.

`displayRun :: Run -> String`

`displayPeg :: Peg -> Run -> String`

`showPlayer :: Player -> String`

`charToPeg :: Char -> Maybe Peg`

The `displayRun`

displays the playing board that resulted from the given run.
The `displayPeg`

is its utility function which displays
a specific position on the board.

`showPlayer`

displays the name of a player.

`charToPeg`

converts a character input into a Peg.
The characters from 1 to 9 are interpreted as motions,
whereas remaining characters are not interpreted as anything
and are invalid to give as an input.

Below's the whole program printout.

Before you read it, keep in mind that I haven't told you anything about how to comprehend the program -part here. I only told you what the types mean.

If you're not familiar with Haskell, likely only the lines I explained make any sense, but those are also the lines that are easiest to understand and they explain how this program is glued together.

There's also bit more to reading Haskell types than presented here. I tried to give an experience of what it'd be like to comprehend programs from their types. This is not enough to teach you Haskell.

`module Main where`

`import Data.Monoid ((<>))`

`import Control.Monad (guard, (>=>))`

`-- Valid tic-tac-toe game:`

`-- players take turns, placing pegs.`

`-- first player places crosses.`

`-- second player places circles.`

`-- a peg cannot be placed over an existing peg.`

`-- peg must be placed within bounds.`

`-- player wins if he places his pegs such that his pegs forms a line of three.`

`type Run = [Peg]`

`type Peg = (Integer, Integer)`

`data Player = Cross | Circle`

`whoseTurnItIs :: Run -> Player`

`whoseTurnItIs [] = Cross`

`whoseTurnItIs (_:[]) = Circle`

`whoseTurnItIs (_:_:xs) = whoseTurnItIs xs`

`priorMoves :: Run -> [Peg]`

`priorMoves [] = []`

`priorMoves (_:[]) = []`

`priorMoves (_:x:xs) = x : priorMoves xs`

`isValidMove :: Run -> Peg -> Bool`

`isValidMove run m = case (inBounds m, peg m run) of`

`(True, Nothing) -> True`

`_ -> False`

`isWinningMove :: Run -> Peg -> Bool`

`isWinningMove run peg`

`= let moves = priorMoves run`

`in length (filter (line 1 0 peg) moves) == 2`

`|| length (filter (line 0 1 peg) moves) == 2`

`|| length (filter (line 1 1 peg) moves) == 2`

`|| length (filter (line 1 (-1) peg) moves) == 2`

`line :: Integer -> Integer -> Peg -> Peg -> Bool`

`line i j (x,y) (z,w) = (x*i + y*j == z*i + w*j)`

`inBounds :: Peg -> Bool`

`inBounds (x, y) = (0 <= x && x < 3 && 0 <= y && x < 3)`

`bounds :: [Peg]`

`bounds = (\y x -> (x,y)) <$> [0,1,2] <*> [0,1,2]`

`displayRun :: Run -> String`

`displayRun run = concat`

`(displayPeg <$> bounds <*> pure run)`

`displayPeg :: Peg -> Run -> String`

`displayPeg m@(x,y) run = let`

`text = case peg m run of`

`Nothing -> "."`

`Just Circle -> "O"`

`Just Cross -> "X"`

`in text <> if x==2 then (if y==2 then "\n" else "\n-----\n") else "|"`

`peg :: Peg -> Run -> Maybe Player`

`peg m [] = Nothing`

`peg m (x:xs) = if m == x then Just (whoseTurnItIs xs) else peg m xs`

`showPlayer :: Player -> String`

`showPlayer Circle = "circle"`

`showPlayer Cross = "cross"`

`main :: IO ()`

`main = play []`

`play :: Run -> IO ()`

`play run = do`

`putStrLn (displayRun run)`

`if length run == 9`

`then putStrLn "it is a tie"`

`else do`

`putStr ("move ("<> showPlayer (whoseTurnItIs run) <> "): ")`

`pegp <- (charToPeg >=> check (isValidMove run)) <$> getChar`

`putStrLn ""`

`case pegp of`

`Nothing -> putStrLn "bad move" >> play run`

`Just peg ->`

`if isWinningMove run peg`

`then putStrLn (displayRun (peg:run)) >> putStrLn "you won"`

`else play (peg:run)`

`check :: (a -> Bool) -> a -> Maybe a`

`check f x = if f x then Just x else Nothing`

`charToPeg :: Char -> Maybe Peg`

`charToPeg '1' = Just (0,0)`

`charToPeg '2' = Just (1,0)`

`charToPeg '3' = Just (2,0)`

`charToPeg '4' = Just (0,1)`

`charToPeg '5' = Just (1,1)`

`charToPeg '6' = Just (2,1)`

`charToPeg '7' = Just (0,2)`

`charToPeg '8' = Just (1,2)`

`charToPeg '9' = Just (2,2)`

`charToPeg _ = Nothing`

If you'd like to test it, you can drop it into
repl.it.
The site fails to interpret `getChar`

like it does in a terminal though.

If you try it out, it looks like this and you control both players through 0-9 -letters:

`.|.|O`

`-----`

`X|.|.`

`-----`

`.|.|.`

`move (cross):`

I guess people will be doubtful about this prediction, but I got my excuse to write a program that plays noughts and crosses.