Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
drawing_arrows_and_coding_functions [2016/09/21 16:50] nikolaj |
drawing_arrows_and_coding_functions [2016/09/21 16:51] nikolaj old revision restored (2016/09/21 16:49) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ===== Drawing arrows and coding functions ===== | + | ===== A type system as a model for some concepts ===== |
| - | | [[Outline]] $\blacktriangleright$ Drawing arrows and coding functions $\blacktriangleright$ [[A type system as a model for some concepts]] | | + | | [[Drawing arrows and coding functions]] $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ [[Foundational temp1 ]] | |
| ==== Guide ==== | ==== Guide ==== | ||
| (We introduce some basic notions of Idris and discuss it in terms of some category theoretical notions, as discussed in | (We introduce some basic notions of Idris and discuss it in terms of some category theoretical notions, as discussed in | ||
| [[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]. | [[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]. | ||
| The code presented below is also all included on the page [[Idris syntax]].) | The code presented below is also all included on the page [[Idris syntax]].) | ||
| - | |||
| - | == What will eventually be used here == | ||
| - | |||
| - | 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 | ||
| - | |||
| - | === 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 == | ||
| - | |||
| - | <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}$ | ||
| === tmp Overview === | === tmp Overview === | ||
| Line 245: | Line 112: | ||
| ----- | ----- | ||
| - | === Related === | ||
| - | [[Idris syntax]] | ||
| === Sequel of === | === Sequel of === | ||
| - | [[Outline]] | + | [[Drawing arrows and coding functions]] |
