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

Here some type judgements and also some drawings.

We draw graph pictures that display parts of our type system.

Make a more elaborate picture with a circle and some element, and an outer circle for Type.
Later, draw a similar picture wiht a function (+ element wise maps of it)

E.g. the type of integers are part of our system and may we draw the vertex $$ {\mathbb Z} $$

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}$

Idris syntax

Outline