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:50] 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 ==== | ||
- | (We introduce some basic notions of Idris and discuss it in terms of some category theoretical notions, as discussed in | + | === Type system === |
- | [[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]. | + | 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". |
- | The code presented below is also all included on the page [[Idris syntax]].) | + | |
- | == What will eventually be used here == | + | >do int and maybe string |
- | Four languages: | + | == Intuitive introductory example == |
- | + | ||
- | - 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. | Here some type judgements and also some drawings. | ||
Line 138: | Line 115: | ||
${\mathbb Z}:{\rm Type}$ | ${\mathbb Z}:{\rm Type}$ | ||
- | |||
- | === tmp Overview === | ||
- | == easy == | ||
- | |||
- | * 2 There is a set {0} with exactly one element | ||
- | * 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) == | ||
- | |||
- | * 8 The subsets of a set X correspond to the functions from X to {0,1} (subobject classifier pullback) | ||
- | * 7 Given f:X->Y and y:Y, one can form the inverse image of f (pullback with {0} on one side) | ||
- | |||
- | == harder (ew) == | ||
- | |||
- | * 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) | ||
- | * 4 A function is determined by its effect on elements (muh (function) extensionality) | ||
- | |||
- | |||
- | |||
- | |||
- | |||
- | === Types === | ||
- | >Want to talk about functions, need types | ||
- | |||
- | == Finite types == | ||
- | >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 | ||
- | |||
- | == Unit type == | ||
- | == Empty type == | ||
- | |||
- | === Functions === | ||
- | == 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. | ||
- | |||
- | == introduce dependent types == | ||
- | |||
- | == Pullback == | ||
- | <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 | ||
- | square n = n*n | ||
- | |||
- | aSolution : Pullback Test.times8 Test.square | ||
- | 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 | ||
- | --willNotCompile = MkPullback 3 5 Refl | ||
- | -- The compiler reduces '3*8 = 5*5' to '24 = 25' and then down to '0 = 1' | ||
- | -- but there is actually no way to prove this. In particular, Refl won't do | ||
- | </code> | ||
- | {{pullback_category_theory.png?X250 }} | ||
- | |||
- | == Product == | ||
- | >cheap product | ||
- | >actual product syntax | ||
- | |||
- | == injections, subsets == | ||
- | |||
- | == Nats == | ||
- | (infinitely large type) | ||
- | |||
- | === Properties === | ||
- | using dependent types, prove the properties discussed below (if possible) | ||
- | |||
- | == of Functions == | ||
- | >identity exists | ||
- | >associations | ||
- | |||
- | == of Types == | ||
- | >of empty | ||
- | >of unit | ||
- | >of product | ||
- | >of exponential object | ||
- | >of Nat | ||
- | |||
- | == caty == | ||
- | >all of the above in terms of universal properties | ||
- | |||
- | === More on Functions === | ||
- | >Type level functions (type constructors) | ||
- | |||
- | >Functors | ||
- | >Monads | ||
=== Reference === | === Reference === | ||
- | ArXiv: | ||
- | [[http://arxiv.org/abs/1212.6543|Leinster, Rethinking set theory]] | ||
----- | ----- |