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


Idris syntax

Sequel of

Outline