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:51] nikolaj old revision restored (2016/09/21 16:49) |
drawing_arrows_and_coding_functions [2016/09/21 16:52] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ===== A type system as a model for some concepts ===== | + | ===== Drawing arrows and coding functions ===== |
| - | | [[Drawing arrows and coding functions]] $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ [[Foundational temp1 ]] | | + | | [[Outline]] $\blacktriangleright$ Drawing arrows and coding functions $\blacktriangleright$ [[A type system as a model for some concepts]] | |
| ==== Guide ==== | ==== Guide ==== | ||
| - | (We introduce some basic notions of Idris and discuss it in terms of some category theoretical notions, as discussed in | + | == What will eventually be used here == |
| - | [[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]. | + | |
| - | The code presented below is also all included on the page [[Idris syntax]].) | + | |
| - | === tmp Overview === | + | Four languages: |
| - | == easy == | + | |
| - | * 2 There is a set {0} with exactly one element | + | - proper cat'ish drawing |
| - | * 3 There is a set {} with no elements | + | |
| - | * 6 Given sets X and Y, one can form the set of functions from X to Y | + | |
| - | * 5 Given sets X and Y, one can form their Cartesian product X x Y (pullback with {0} in the middle) | + | |
| - | * 9 The natural numbers form a set | + | |
| - | * 1 Composition of functions is associative and there are identity functions | + | |
| - | == harder (needs dependent types) == | + | $$ |
| + | \require{AMScd} | ||
| - | * 8 The subsets of a set X correspond to the functions from X to {0,1} (subobject classifier pullback) | + | \begin{CD} |
| - | * 7 Given f:X->Y and y:Y, one can form the inverse image of f (pullback with {0} on one side) | + | {\large\hbar} @>{\large{!}}>> {\large{*}} |
| + | \\ | ||
| + | @V{{\large{m}}}VV @VV{{\large\top}}V | ||
| + | \\ | ||
| + | {\large\heartsuit} @>>{\large{\chi}}> {\large{\Omega}} | ||
| + | \end{CD} | ||
| + | $$ | ||
| - | == harder (ew) == | + | - drawing where you see terms, circled (the type universe is circled as well) |
| - | * 10 Every surjection has a right inverse (muh axiom of choice, easy if surjective functions are defined as function type where surjectivity must be proven for terms) | + | - typey syntax |
| - | * 4 A function is determined by its effect on elements (muh (function) extensionality) | + | |
| + | - 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 == | ||
| - | === Types === | + | <code/Haskell> |
| - | >Want to talk about functions, need types | + | i : Integer |
| + | i = 13 | ||
| - | == Finite types == | + | k : Integer |
| - | >Beagle, Kid | + | k = 4 |
| - | >Draw the corresponding arrows (akin to Lawyeres babby book) | + | |
| - | >For any number {0, 1, 2, 3, ..., 17, 18, ...} we can form a type with that many terms | + | n : Integer |
| + | n = 2 + 3 | ||
| - | == Unit type == | + | m : Integer |
| - | == Empty type == | + | m = -70 + n |
| + | </code> | ||
| - | === Functions === | + | $13 : {\mathbb Z}$ |
| - | == Function type == | + | |
| - | >basic function definition (forth, back, permutation, identity) | + | |
| - | >Draw the corresponding arrows (akin to Lawyeres babby book) | + | |
| - | >given $f:X\to Y$, point out how $i:S\to{X}$ and $j:X\to{T}$ induces functions $(f\circ{i}):S\to Y$, $(j\circ{f}):X\to T$ with potentially restricted domain resp. codomain. It's always interesting to see how a given function $g$ may factor into other functions. Parts of "factors" may be general and important functions, defined for very general input, or e.g. components of natural transformations, etc. | + | $4 : {\mathbb Z}$ |
| - | == introduce dependent types == | + | $k:=4$ |
| - | == Pullback == | + | $k : {\mathbb Z}$ |
| - | <code/Haskell> | + | |
| - | data Pullback : (f : x -> z) -> (g : y -> z) -> Type | + | |
| - | where MkPullback : (tx : x) -> (ty : y) -> (f tx = g ty) -> (Pullback f g) | + | |
| - | -- MkPullback maps a term tx, a term ty and a proof | + | |
| - | -- that f tx = g ty to a global element of Pullback f g | + | |
| - | + | ||
| - | times8 : Nat -> Nat | + | |
| - | times8 k = k*8 | + | |
| - | square : Nat -> Nat | + | $(2+3) : {\mathbb Z}$ |
| - | square n = n*n | + | |
| - | aSolution : Pullback Test.times8 Test.square | + | $n:=2+3$ |
| - | aSolution = MkPullback 2 4 Refl | + | |
| - | -- The compiler already reduces the type '2*8 = 4*4' to '16 = 16' and Refl proves this | + | |
| - | --willNotCompile : Pullback Test.times8 Test.square | + | $n : {\mathbb Z}$ |
| - | --willNotCompile = MkPullback 3 5 Refl | + | |
| - | -- The compiler reduces '3*8 = 5*5' to '24 = 25' and then down to '0 = 1' | + | <code/Haskell> |
| - | -- but there is actually no way to prove this. In particular, Refl won't do | + | fun : Integer -> Integer |
| + | fun x = x + m | ||
| + | |||
| + | g : Integer -> Integer | ||
| + | g x = -x + k | ||
| + | |||
| + | h : Integer -> Integer | ||
| + | h x = 100 + fun x | ||
| </code> | </code> | ||
| - | {{pullback_category_theory.png?X250 }} | ||
| - | == Product == | + | $g : {\mathbb Z}\to{\mathbb Z}$ |
| - | >cheap product | + | |
| - | >actual product syntax | + | |
| - | == injections, subsets == | + | 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 | ||
| - | == Nats == | + | $({\mathbb Z}\to{\mathbb Z}) : {\rm Type}$ |
| - | (infinitely large type) | + | |
| - | === Properties === | + | <code/Haskell> |
| - | using dependent types, prove the properties discussed below (if possible) | + | 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 | ||
| - | == of Functions == | + | $(({\mathbb Z}\to{\mathbb Z})\to{\mathbb Z}) : {\rm Type}$ |
| - | >identity exists | + | |
| - | >associations | + | |
| - | == of Types == | + | Actualy, in this system we have |
| - | >of empty | + | |
| - | >of unit | + | |
| - | >of product | + | |
| - | >of exponential object | + | |
| - | >of Nat | + | |
| - | == caty == | + | ${\rm Type}:{\rm Type}$ |
| - | >all of the above in terms of universal properties | + | |
| - | === More on Functions === | + | and we so may draw |
| - | >Type level functions (type constructors) | + | $$ |
| + | {\rm Type} | ||
| + | $$ | ||
| + | and write | ||
| - | >Functors | + | ${\mathbb Z}:{\rm Type}$ |
| - | >Monads | + | |
| === Reference === | === Reference === | ||
| - | ArXiv: | ||
| - | [[http://arxiv.org/abs/1212.6543|Leinster, Rethinking set theory]] | ||
| ----- | ----- | ||
| + | === Related === | ||
| + | [[Idris syntax]] | ||
| === Sequel of === | === Sequel of === | ||
| - | [[Drawing arrows and coding functions]] | + | [[Outline]] |
