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

Reference


Sequel of

Link to graph
Log In
Improvements of the human condition