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.