410 lines
12 KiB
HTML
410 lines
12 KiB
HTML
<!DOCTYPE html>
|
||
<html>
|
||
<head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge,chrome=1">
|
||
<meta name="viewport" content="width=1024, user-scalable=no">
|
||
|
||
<title>Category Theory for Programming</title>
|
||
|
||
<!-- Required stylesheet -->
|
||
<link rel="stylesheet" href="core/deck.core.css">
|
||
|
||
<!-- Extension CSS files go here. Remove or add as needed. -->
|
||
<link rel="stylesheet" href="extensions/goto/deck.goto.css">
|
||
<link rel="stylesheet" href="extensions/menu/deck.menu.css">
|
||
<link rel="stylesheet" href="extensions/navigation/deck.navigation.css">
|
||
<link rel="stylesheet" href="extensions/status/deck.status.css">
|
||
<link rel="stylesheet" href="extensions/hash/deck.hash.css">
|
||
<link rel="stylesheet" href="extensions/scale/deck.scale.css">
|
||
|
||
<!-- Transition theme. More available in /themes/transition/ or create your own. -->
|
||
|
||
<link rel="stylesheet" href="themes/transition/fade.css">
|
||
<!-- Style theme. More available in /themes/style/ or create your own. -->
|
||
<!-- <link rel="stylesheet" href="themes/style/web-2.0.css"> -->
|
||
<link rel="stylesheet" href="themes/style/y/main.css" />
|
||
<link rel="stylesheet" href="themes/style/y/solarized.css" />
|
||
|
||
<!-- Required Modernizr file -->
|
||
<script src="modernizr.custom.js"></script>
|
||
|
||
</head>
|
||
<body class="deck-container">
|
||
|
||
<div style="display:none">
|
||
\(\newcommand{\F}{\mathbf{F}}\)
|
||
\(\newcommand{\C}{\mathcal{C}}\)
|
||
\(\newcommand{\D}{\mathcal{D}}\)
|
||
\(\newcommand{\id}{\mathrm{id}}\)
|
||
\(\newcommand{\ob}[1]{\mathrm{ob}(#1)}\)
|
||
\(\newcommand{\hom}[1]{\mathrm{hom}(#1)}\)
|
||
\(\newcommand{\Set}{\mathbf{Set}}\)
|
||
</div>
|
||
|
||
|
||
<!-- Begin slides. Just make elements with a class of slide. -->
|
||
|
||
<section class="slide">
|
||
<h1>Category Theory <span class="and"><span class="and">&</span></span> Programming
|
||
<div><author style="font-size: .4em"><em class="base01">by</em> Yann Esposito
|
||
<div>
|
||
<twitter style="font-size: .5em">
|
||
<a href="http://twitter.com/yogsototh">@yogsototh</a>,
|
||
</twitter>
|
||
<googleplus style="font-size: .5em">
|
||
<a href="https://plus.google.com/117858550730178181663">+yogsototh</a>
|
||
</googleplus>
|
||
</div>
|
||
</author></div>
|
||
</h1>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Plan</h2>
|
||
<ul style="font-size: 2em">
|
||
<li class="yellow">Why?</li>
|
||
<li>What?</li>
|
||
<li>How?</li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Abstraction</h2>
|
||
<p>A common concept you see often in multiple instances.</p>
|
||
<div class="slide">
|
||
<p>Numbers: 1,2,3,... <em class="small">3400 BC, real numbers 760 BC</em></p>
|
||
<figure class="left">
|
||
<img src="categories/img/tally-count.png" style="height:5em" alt="Aboriginal Tally System"/>
|
||
<figcaption>Aboriginal Tally System</figcaption>
|
||
</figure>
|
||
<div class="slide">
|
||
<div class="left">amelioration ⇒</div>
|
||
<figure class="left">
|
||
<img src="categories/img/first-real-numbers.png" style="height:5em" alt="Mesopotamian Numbers"/>
|
||
<figcaption>Mesopotamian base 60 system</figcaption>
|
||
</figure>
|
||
</div>
|
||
<div class="flush"></div>
|
||
<div class="slide">
|
||
Operators: <b>=, <, >, +, ×, ...</b>
|
||
</div>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Abstraction</h2>
|
||
<h3>Generalizations</h3>
|
||
<div class="right">
|
||
<img src="categories/img/egyptian-hieroglyphics.jpg" alt="Egyptian Fractions"/>
|
||
<img src="categories/img/negative-numbers.jpg" alt="Negative Numbers (Chinese)"/>
|
||
</div>
|
||
<ul>
|
||
<li>Rational (Weight/Distance/Time): \(\frac{p}{q}\)
|
||
</li>
|
||
<li>Negative (Debts): ..., -2, -1, ? , 1, 2, ...
|
||
</li>
|
||
<li>Irrational (Geometry): 500 BC, Pythogoras killed Hippasus for \(\sqrt{2}\)</li>
|
||
<li>Complex (Algebra): \(\mathbb{C}\) ; 100 AD, then 16th century</li>
|
||
<li>\(0\): nothing become a number!</li>
|
||
</ul>
|
||
<p><b>More "things" can be understood as numbers</b></p>
|
||
<p><b>More "operator" to manipulate numbers</b></p>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Numbers ⇒ Sets</h2>
|
||
<table>
|
||
<tr>
|
||
<th>Numbers</th>
|
||
<th>Set Theory (∞)/Abstract Algebra/Topology</th>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{N}\): \((+,0)\)</td>
|
||
<td>Semigroups</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{Z}\): \((+,0,\times,1)\)</td>
|
||
<td>Rings</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{Q}\)</td>
|
||
<td>Fields</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{R}\)</td>
|
||
<td>Complete Fields (<em class="base01">topology</em>)</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{C}\)</td>
|
||
<td>Algebræ</td>
|
||
</tr>
|
||
<tr><td></td><td>Modules,Vector Spaces, Monoids, ...</td></tr>
|
||
</table>
|
||
<p><span class="and" style="visibility:hidden"><span class="and">&</span></span> More <strong>general</strong>: more things are sets.<br/>
|
||
<span class="and"><span class="and">&</span></span> More <strong>precise</strong>: clear distinction between concepts.</p>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Sets ⇒? <span class="yellow">Categories</span></h2>
|
||
<table>
|
||
<tr>
|
||
<th>Numbers</th>
|
||
<th>Sets</th>
|
||
<th>Categories</th>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{N}\): \((+,0)\)</td>
|
||
<td>Semigroups</td>
|
||
<td>?</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{Z}\): \((+,0,\times,1)\)</td>
|
||
<td>Rings</td>
|
||
<td>?</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{Q}\)</td>
|
||
<td>Fields</td>
|
||
<td>?</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{R}\)</td>
|
||
<td>Complete Fields (<em class="base01">topology</em>)</td>
|
||
<td>?</td>
|
||
</tr>
|
||
<tr>
|
||
<td>\(\mathbb{C}\)</td>
|
||
<td>Algebræ</td>
|
||
<td>?</td>
|
||
</tr>
|
||
<tr><td></td><td>Modules,Vector Spaces, Monoids, ...</td><td>?</td></tr>
|
||
</table>
|
||
</section>
|
||
<section class="slide">
|
||
<h2><span class="yellow">/.*/</span> ⇒? Category Theory</h2>
|
||
<p>Extend <span class="and"><span class="and">&</span></span> Merge different scientific fields</p>
|
||
<ul>
|
||
<li>Topology</li>
|
||
<li>Quantum Physics</li>
|
||
<li>Logic</li>
|
||
<li><b>Programming</b></li>
|
||
</ul>
|
||
<p><span class="and" style="visibility:hidden"><span class="and">&</span></span> More <strong>general</strong>: more things are Categories.<br/>
|
||
<span class="and"><span class="and">&</span></span> More <strong>precise</strong>: better distinction between concepts.</p>
|
||
<p>Young field: <b>1942–45</b>, Samuel Eilenberg <span class="and"><span class="and">&</span></span> Saunders Mac Lane
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Type Theory ⇒ Categories</h2>
|
||
|
||
<ul>
|
||
<li>Type theory helped to remove paradoxes in Set Theory.</li>
|
||
<li>Prevent relations between different kind of objects.</li>
|
||
<li>Used in computer science</li>
|
||
</ul>
|
||
|
||
<ul>
|
||
<li>typed λ-calculus ⇒ cartesian closed categories</li>
|
||
<li>untyped λ-calculus ⇒ C-monoids (subclass of categories)</li>
|
||
<li>Martin-Löf type theories ⇒ locally cartesian closed categories</li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Category Definition</h2>
|
||
|
||
<p> A Category \(\mathcal{C}\) is defined by:</p>
|
||
<ul>
|
||
<li> <em>Objects (\(\ob{C}\))</em>,</li>
|
||
<li> <em>Morphisms (\(\hom{C}\))</em>,</li>
|
||
<li> a <em>Composition law (∘)</em></li>
|
||
<li> obeying some <em>Properties</em>.</li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Plan</h2>
|
||
<ul style="font-size: 2em">
|
||
<li>Why?</li>
|
||
<li class="yellow">What?</li>
|
||
<li>How?</li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Category Definition: Objects</h2>
|
||
|
||
<img src="categories/img/mp/objects.png" alt="objects" />
|
||
|
||
<p>\(\ob{\mathcal{C}}\) is a collection</p>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Category Definition: Morphisms</h2>
|
||
|
||
<img src="categories/img/mp/morphisms.png" alt="morphisms"/>
|
||
|
||
<p>\(\hom{A,B}\) is a collection</p>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Category Definition: Composition</h2>
|
||
<p>Composition (∘): \(f:A\rightarrow B, g:B\rightarrow C\)
|
||
$$g\circ f:A\rightarrow C$$
|
||
</p>
|
||
<img src="categories/img/mp/composition.png" alt="composition"/>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Category laws: neutral element</h2>
|
||
<p>for all \(X\), there is an \(\id_X\), s.t. for all \(f:A\to B\):</p>
|
||
<img src="categories/img/mp/identity.png" alt="identity"/>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Category laws: Associativity</h2>
|
||
<p> Composition is associative:</p>
|
||
<img src="categories/img/mp/associativecomposition.png" alt="associative composition"/>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Can this be a category? <span style="font-size: .5em">(\(\id_X\) implicit)</span></h2>
|
||
<figure class="left">
|
||
<img src="categories/img/mp/cat-example1.png" alt="Category example 1"/>
|
||
<figcaption class="slide">
|
||
<span class="green">OK</span>
|
||
</figcaption>
|
||
</figure>
|
||
<figure class="left">
|
||
<img src="categories/img/mp/cat-example2.png" alt="Category example 2"/>
|
||
<figcaption class="slide">
|
||
no candidate for \(g\circ f\)
|
||
<span class="red">NO</span>
|
||
</figcaption>
|
||
</figure>
|
||
<figure class="left">
|
||
<img src="categories/img/mp/cat-example3.png" alt="Category example 3"/>
|
||
<figcaption class="slide">
|
||
<span class="green">YES</span>
|
||
</figcaption>
|
||
</figure>
|
||
<figure class="left">
|
||
<img src="categories/img/mp/cat-example4.png" alt="Category example 4"/>
|
||
<figcaption class="slide">
|
||
no candidate for \(f:C\to B\)
|
||
<span class="red">NO</span>
|
||
</figcaption>
|
||
</figure>
|
||
<figure class="left">
|
||
<img src="categories/img/mp/cat-example5.png" alt="Category example 5"/>
|
||
<figcaption class="slide">
|
||
\((h∘g)∘f=\id_B∘f=f≠h=h∘\id_A=h∘(g∘f)\)
|
||
<span class="red">NO</span>
|
||
</figcaption>
|
||
</figure>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Categories Everywhere?</h2>
|
||
|
||
<h3>\(\Set\)</h3>
|
||
<ul>
|
||
<li> \(\ob{\Set}\) are sets</li>
|
||
<li> \(\hom{\Set}\) are functions</li>
|
||
<li> ∘ is functions composition </li>
|
||
</ul>
|
||
|
||
<ul class="slide">
|
||
<li>\(\ob{\Set}\) is a proper class ; not a set</li>
|
||
<li>\(\hom{E,F}\) is a set</li>
|
||
<li>\(\Set\) is a <em>locally small category</em></li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Categories Everywhere?</h2>
|
||
|
||
<h3>Strings</h3>
|
||
<ul>
|
||
<li> \(\ob{Str}\) is a singleton </li>
|
||
<li> \(\hom{Str}\) each string </li>
|
||
<li> ∘ is concatenation <code>(++)</code> </li>
|
||
</ul>
|
||
<ul>
|
||
<li> <code>"" ++ u = u = u ++ ""</code> </li>
|
||
<li> <code>(u ++ v) ++ w = u ++ (v ++ w)</code> </li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Definition: Functor</h2>
|
||
|
||
<p> A functor is a mapping between two categories.
|
||
Let \(\C\) and \(\D\) be two categories.
|
||
A <em>functor</em> \(\F\) from \(\C\) to \(\D\):</p>
|
||
<ul>
|
||
<li> Associate objects: \(A\in\ob{\C}\) to \(\F(A) \in\ob{\D}\) </li>
|
||
<li> Associate morphisms: \(f:A\to B\) to \(\F(f) : \F(A) \to \F(B)\)
|
||
such that
|
||
<ul>
|
||
<li>\( \F (\id_X) = \id_{\F(X)} \),</li>
|
||
<li>\( \F (g \circ_\C f) = \F(g) \circ_\D \F(f) \)</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Functor: Example</h2>
|
||
|
||
<img src="categories/img/mp/functor.png" alt="Functor"/>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Functor: Example</h2>
|
||
|
||
<img src="categories/img/mp/functor-morphism.png" alt="Functor"/>
|
||
</section>
|
||
<section class="slide">
|
||
<h2>Functor: Example</h2>
|
||
|
||
<img src="categories/img/mp/functor-morphism-color.png" alt="Functor"/>
|
||
</section>
|
||
<!-- End slides. -->
|
||
|
||
|
||
<!-- Begin extension snippets. Add or remove as needed. -->
|
||
|
||
<!-- deck.navigation snippet -->
|
||
<a href="#" class="deck-prev-link" title="Previous">←</a>
|
||
<a href="#" class="deck-next-link" title="Next">→</a>
|
||
|
||
<!-- deck.status snippet -->
|
||
<p class="deck-status">
|
||
<span class="deck-status-current"></span>
|
||
/
|
||
<span class="deck-status-total"></span>
|
||
</p>
|
||
|
||
<!-- deck.goto snippet -->
|
||
<form action="." method="get" class="goto-form">
|
||
<label for="goto-slide">Go to slide:</label>
|
||
<input type="text" name="slidenum" id="goto-slide" list="goto-datalist">
|
||
<datalist id="goto-datalist"></datalist>
|
||
<input type="submit" value="Go">
|
||
</form>
|
||
|
||
<!-- deck.hash snippet -->
|
||
<a href="." title="Permalink to this slide" class="deck-permalink">#</a>
|
||
|
||
<!-- End extension snippets. -->
|
||
|
||
|
||
<!-- Required JS files. -->
|
||
<script src="jquery-1.7.2.min.js"></script>
|
||
<script src="core/deck.core.js"></script>
|
||
|
||
<!-- Extension JS files. Add or remove as needed. -->
|
||
<script src="core/deck.core.js"></script>
|
||
<script src="extensions/hash/deck.hash.js"></script>
|
||
<script src="extensions/menu/deck.menu.js"></script>
|
||
<script src="extensions/goto/deck.goto.js"></script>
|
||
<script src="extensions/status/deck.status.js"></script>
|
||
<script src="extensions/navigation/deck.navigation.js"></script>
|
||
<script src="extensions/scale/deck.scale.js"></script>
|
||
|
||
<!-- Initialize the deck. You can put this in an external file if desired. -->
|
||
<script>
|
||
$(function() {
|
||
$.deck('.slide');
|
||
});
|
||
</script>
|
||
<!-- Y theme -->
|
||
<script src="js/mathjax/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
|
||
<script src="js/highlight/highlight.pack.js"></script>
|
||
<script>
|
||
hljs.initHighlightingOnLoad();
|
||
</script>
|
||
</body>
|
||
</html>
|