Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
drawing_arrows_and_coding_functions [2016/09/21 16:52] nikolaj |
drawing_arrows_and_coding_functions [2016/10/15 14:23] nikolaj |
||
---|---|---|---|
Line 2: | Line 2: | ||
| [[Outline]] $\blacktriangleright$ Drawing arrows and coding functions $\blacktriangleright$ [[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]] | | ||
==== Guide ==== | ==== Guide ==== | ||
- | == What will eventually be used here == | + | === 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". | ||
- | Four languages: | + | >do int and maybe string |
- | - proper cat'ish drawing | + | == Intuitive introductory example == |
- | + | ||
- | $$ | + | |
- | \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. | Here some type judgements and also some drawings. | ||