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
What will eventually be used here
move to former page
Four languages:
- proper cat'ish drawing
$$ \require{AMScd} \begin{CD} {\large\hbar} @>{\large{!}}>> {\large{*}} \\ @V{{\large{m}}}VV @VV{{\large\top}}V \\ {\large\heartsuit} @>>{\large{\chi}}> {\large{\Omega}} \end{CD} $$
- drawing where you see terms, circled (the type universe is circled as well)
- typey syntax
- FOL/SOL
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}$