This is an old revision of the document!

## Drawing arrows and coding functions

 Outline $\blacktriangleright$ Drawing arrows and coding functions $\blacktriangleright$ A type system as a model for some concepts

### Guide

#### Type system

A main part of a type system is a collection of names that stand for so called types. We will draw a lot of simple pictures with those types “lying around”.

do int and maybe string
##### Intuitive introductory example

Here some type judgements and also some drawings.

##### The type Type

We draw graph pictures that display parts of our type system. E.g. the type of integers are part of our system and may we draw the vertex $${\mathbb Z}$$

##### Addition and substraction of integers
i : Integer
i = 13

k : Integer
k = 4

n : Integer
n = 2 + 3

m : Integer
m = -70 + n

$13 : {\mathbb Z}$

$4 : {\mathbb Z}$

$k:=4$

$k : {\mathbb Z}$

$(2+3) : {\mathbb Z}$

$n:=2+3$

$n : {\mathbb Z}$

fun : Integer -> Integer
fun x = x + m

g : Integer -> Integer
g x = -x + k

h : Integer -> Integer
h x = 100 + fun x

$g : {\mathbb Z}\to{\mathbb Z}$

The function $g$ is one of an unending list of possible functions from ${\mathbb Z}$ to ${\mathbb Z}$ that we can define. Draw $${\mathbb Z}\longrightarrow{\mathbb Z}$$ or $$\require{AMScd} \begin{CD} {\mathbb Z} \\ @V{{}}VV \\ {\mathbb Z} \end{CD}$$ and then

$({\mathbb Z}\to{\mathbb Z}) : {\rm Type}$

F : (Integer -> Integer) -> Integer
F f = 5000 + f k

Draw $$({\mathbb Z}\to{\mathbb Z})\longrightarrow{\mathbb Z}$$ or $$\require{AMScd} \begin{CD} ({\mathbb Z}\to{\mathbb Z}) \\ @V{{}}VV \\ {\mathbb Z} \end{CD}$$ and then

$(({\mathbb Z}\to{\mathbb Z})\to{\mathbb Z}) : {\rm Type}$

Actualy, in this system we have

${\rm Type}:{\rm Type}$

and we so may draw $${\rm Type}$$ and write

${\mathbb Z}:{\rm Type}$