===== 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. 

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

== Addition and substraction of integers ==

<code/Haskell>
i : Integer
i = 13

k : Integer
k = 4

n : Integer
n = 2 + 3

m : Integer
m = -70 + n
</code>

$13 : {\mathbb Z}$

$4 : {\mathbb Z}$

$k:=4$

$k : {\mathbb Z}$

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

$n:=2+3$

$n : {\mathbb Z}$

<code/Haskell>
fun : Integer -> Integer
fun x = x + m

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

h : Integer -> Integer
h x = 100 + fun x
</code>

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

<code/Haskell>
F : (Integer -> Integer) -> Integer
F f = 5000 + f k
</code>
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}$

=== Reference ===

-----
=== Related ===
[[Idris syntax]]
=== Sequel of ===
[[Outline]]