Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next 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/10/14 09:24] nikolaj [Guide] |
||
---|---|---|---|
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 === | + | >move to former page |
- | == easy == | + | Four languages: |
- | * 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 | ||
+ | === 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. | ||
- | === Types === | + | == The type Type == |
- | >Want to talk about functions, need types | + | 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} | ||
+ | $$ | ||
- | == Finite types == | + | == Addition and substraction of integers == |
- | >Beagle, Kid | + | |
- | >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 | + | <code/Haskell> |
+ | i : Integer | ||
+ | i = 13 | ||
- | == Unit type == | + | k : Integer |
- | == Empty type == | + | k = 4 |
- | === Functions === | + | n : Integer |
- | == Function type == | + | n = 2 + 3 |
- | >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. | + | m : Integer |
+ | m = -70 + n | ||
+ | </code> | ||
- | == introduce dependent types == | + | $13 : {\mathbb Z}$ |
- | == Pullback == | + | $4 : {\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 | + | $k:=4$ |
- | square n = n*n | + | |
- | aSolution : Pullback Test.times8 Test.square | + | $k : {\mathbb Z}$ |
- | 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 | + | $(2+3) : {\mathbb Z}$ |
- | --willNotCompile = MkPullback 3 5 Refl | + | |
- | -- The compiler reduces '3*8 = 5*5' to '24 = 25' and then down to '0 = 1' | + | $n:=2+3$ |
- | -- but there is actually no way to prove this. In particular, Refl won't do | + | |
+ | $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> | </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]] |