updating
This commit is contained in:
parent
9af0e64001
commit
e5d455c2fd
23 changed files with 173 additions and 49 deletions
|
@ -43,7 +43,7 @@
|
|||
}
|
||||
</script>
|
||||
</head>
|
||||
<body id="body" class="deck-container" style="width: 99%">
|
||||
<body id="body" class="deck-container">
|
||||
|
||||
<div style="display:none">
|
||||
\(\newcommand{\F}{\mathbf{F}}\)
|
||||
|
@ -89,7 +89,7 @@
|
|||
<ul style="font-size: 2em; font-weight:bold">
|
||||
<li><span class="yellow">Why?
|
||||
<ul class="base01" style="border-left: 2px solid; padding-left: 1em; font-size: .6em; float: right; font-weight: bold; margin: 0 0 0 1em">
|
||||
<li>General overview</li>
|
||||
<li class="yellow">General overview</li>
|
||||
<li>Math <span class="and">&</span> Abstraction</li>
|
||||
<li>Programming <span class="and">&</span> Abstraction</li>
|
||||
<li>Categories <span class="and">&</span> Abstraction</li>
|
||||
|
@ -141,6 +141,21 @@
|
|||
</ul>
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Plan</h2>
|
||||
<ul style="font-size: 2em; font-weight:bold">
|
||||
<li><span class="yellow">Why?
|
||||
<ul class="base01" style="border-left: 2px solid; padding-left: 1em; font-size: .6em; float: right; font-weight: bold; margin: 0 0 0 1em">
|
||||
<li>General overview</li>
|
||||
<li class="yellow">Math <span class="and">&</span> Abstraction</li>
|
||||
<li>Programming <span class="and">&</span> Abstraction</li>
|
||||
<li>Categories <span class="and">&</span> Abstraction</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li>What?</li>
|
||||
<li>How?</li>
|
||||
</ul>
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Math Abstraction</h2>
|
||||
<p>A common concept you see in multiple instances.</p>
|
||||
<div>
|
||||
|
@ -178,6 +193,7 @@
|
|||
</section>
|
||||
<section class="slide">
|
||||
<h2>Numbers ⇒ Sets</h2>
|
||||
<blockquote><strong>Formalism</strong>: A <em>theory</em> is some strings (the axioms), some string manipulation rules, and all strings created by applying these rules to the axioms.</blockquote>
|
||||
<table>
|
||||
<tr>
|
||||
<th>Numbers</th>
|
||||
|
@ -250,16 +266,33 @@
|
|||
</section>
|
||||
<section class="slide">
|
||||
<h2>Category Theory</h2>
|
||||
<p>Categories package entire mathematical theories.</p>
|
||||
<p>Categories package entire mathematical theories.<br/>
|
||||
Theory=(Axioms,<span style="visibility:hidden">Strings</span>Rules,<span style="visibility:hidden">Stri</span>Theorems)<br/>
|
||||
<span style="visibility:hidden">Theory=</span>(Strings,Strings → Strings, Strings)
|
||||
</p>
|
||||
|
||||
<ul>
|
||||
<li>Topology</li>
|
||||
<li>Quantum Physics</li>
|
||||
<li>Logic</li>
|
||||
<li><b>Programming</b></li>
|
||||
<li><b>Computer Science</b></li>
|
||||
</ul>
|
||||
<p>Recent field: <b>1942–45</b>, Samuel Eilenberg <span class="and">&</span> Saunders Mac Lane
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Plan</h2>
|
||||
<ul style="font-size: 2em; font-weight:bold">
|
||||
<li><span class="yellow">Why?
|
||||
<ul class="base01" style="border-left: 2px solid; padding-left: 1em; font-size: .6em; float: right; font-weight: bold; margin: 0 0 0 1em">
|
||||
<li>General overview</li>
|
||||
<li>Math <span class="and">&</span> Abstraction</li>
|
||||
<li class="yellow">Programming <span class="and">&</span> Abstraction</li>
|
||||
<li>Categories <span class="and">&</span> Abstraction</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li>What?</li>
|
||||
<li>How?</li>
|
||||
</ul>
|
||||
<p><span style="visibility:hidden"><span class="and">&</span></span> More <strong>general</strong>: more things are Categories.<br/>
|
||||
<span class="and">&</span> More <strong>precise</strong>: better distinction between concepts.</p>
|
||||
<p>Young field: <b>1942–45</b>, Samuel Eilenberg <span class="and">&</span> Saunders Mac Lane
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Programming <span class="and">&</span> Abstraction</h2>
|
||||
|
@ -268,12 +301,14 @@
|
|||
<ul>
|
||||
<li>Encouraged by imperative paradigms.
|
||||
</li><li>Actions <span class="and">&</span> mutable objects.
|
||||
</li><li>Time is <em>very</em> important: ex. linked list push
|
||||
</li><li>Time is <em>very</em> important<sup>*</sup>.
|
||||
</li><li>Synchronizing things is a challenge.
|
||||
</li>
|
||||
</ul>
|
||||
<p class="yellow">Natural Abstractions: pointers, variables, loop, Objects, Classes...</p>
|
||||
<p>Representation: a data structure changing other time.</p>
|
||||
|
||||
<p class="small">*: Push an element to a linked list for example</p>
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Untyped Pure Programming</h2>
|
||||
|
@ -281,7 +316,7 @@
|
|||
<ul><li> Time is irrelevant by default.
|
||||
</li><li> Mostly static constructions like pipes.
|
||||
</li><li> All pipes can be plugged ⇒ all error at runtime
|
||||
<ul><li> (+ ("foo" 27) 32)
|
||||
<ul><li> (+ 37 "foo")
|
||||
</li><li> Y = λf.(λx.f (x x)) (λx.f (x x))
|
||||
</li><li> Y g = g (Y g)
|
||||
</li></ul>
|
||||
|
@ -290,6 +325,14 @@
|
|||
<p class="yellow">Natural abstraction: higher level functions <span class="and">&</span> equations</p>
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Untyped Pure Programming</h2>
|
||||
|
||||
|
||||
<p style="text-align:center"><code>(+ 42 "foo")</code></p>
|
||||
|
||||
<img src="categories/img/mp/pipe.png" />
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Typed Pure Programming</h2>
|
||||
<ul><li>Add shapes to pipes:
|
||||
<ul><li> <code class="red">4 + ["foo",27]</code> forbidden
|
||||
|
|
|
@ -2,7 +2,7 @@
|
|||
<ul style="font-size: 2em; font-weight:bold">
|
||||
<li><span class="yellow">Why?
|
||||
<ul class="base01" style="border-left: 2px solid; padding-left: 1em; font-size: .6em; float: right; font-weight: bold; margin: 0 0 0 1em">
|
||||
<li>General overview</li>
|
||||
<li class="yellow">General overview</li>
|
||||
<li>Math & Abstraction</li>
|
||||
<li>Programming & Abstraction</li>
|
||||
<li>Categories & Abstraction</li>
|
||||
|
|
13
categories/10_Introduction/060_Plan.html
Normal file
13
categories/10_Introduction/060_Plan.html
Normal file
|
@ -0,0 +1,13 @@
|
|||
<h2>Plan</h2>
|
||||
<ul style="font-size: 2em; font-weight:bold">
|
||||
<li><span class="yellow">Why?
|
||||
<ul class="base01" style="border-left: 2px solid; padding-left: 1em; font-size: .6em; float: right; font-weight: bold; margin: 0 0 0 1em">
|
||||
<li>General overview</li>
|
||||
<li class="yellow">Math & Abstraction</li>
|
||||
<li>Programming & Abstraction</li>
|
||||
<li>Categories & Abstraction</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li>What?</li>
|
||||
<li>How?</li>
|
||||
</ul>
|
|
@ -1,4 +1,5 @@
|
|||
<h2>Numbers ⇒ Sets</h2>
|
||||
<blockquote><strong>Formalism</strong>: A <em>theory</em> is some strings (the axioms), some string manipulation rules, and all strings created by applying these rules to the axioms.</blockquote>
|
||||
<table>
|
||||
<tr>
|
||||
<th>Numbers</th>
|
|
@ -1,11 +0,0 @@
|
|||
<h2>Category Theory</h2>
|
||||
<p>Categories package entire mathematical theories.</p>
|
||||
<ul>
|
||||
<li>Topology</li>
|
||||
<li>Quantum Physics</li>
|
||||
<li>Logic</li>
|
||||
<li><b>Programming</b></li>
|
||||
</ul>
|
||||
<p><span style="visibility:hidden">&</span> More <strong>general</strong>: more things are Categories.<br/>
|
||||
& More <strong>precise</strong>: better distinction between concepts.</p>
|
||||
<p>Young field: <b>1942–45</b>, Samuel Eilenberg & Saunders Mac Lane
|
13
categories/10_Introduction/110_Category_Theory.html
Normal file
13
categories/10_Introduction/110_Category_Theory.html
Normal file
|
@ -0,0 +1,13 @@
|
|||
<h2>Category Theory</h2>
|
||||
<p>Categories package entire mathematical theories.<br/>
|
||||
Theory=(Axioms,<span style="visibility:hidden">Strings</span>Rules,<span style="visibility:hidden">Stri</span>Theorems)<br/>
|
||||
<span style="visibility:hidden">Theory=</span>(Strings,Strings → Strings, Strings)
|
||||
</p>
|
||||
|
||||
<ul>
|
||||
<li>Topology</li>
|
||||
<li>Quantum Physics</li>
|
||||
<li>Logic</li>
|
||||
<li><b>Computer Science</b></li>
|
||||
</ul>
|
||||
<p>Recent field: <b>1942–45</b>, Samuel Eilenberg & Saunders Mac Lane
|
13
categories/10_Introduction/120_Plan.html
Normal file
13
categories/10_Introduction/120_Plan.html
Normal file
|
@ -0,0 +1,13 @@
|
|||
<h2>Plan</h2>
|
||||
<ul style="font-size: 2em; font-weight:bold">
|
||||
<li><span class="yellow">Why?
|
||||
<ul class="base01" style="border-left: 2px solid; padding-left: 1em; font-size: .6em; float: right; font-weight: bold; margin: 0 0 0 1em">
|
||||
<li>General overview</li>
|
||||
<li>Math & Abstraction</li>
|
||||
<li class="yellow">Programming & Abstraction</li>
|
||||
<li>Categories & Abstraction</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li>What?</li>
|
||||
<li>How?</li>
|
||||
</ul>
|
|
@ -4,9 +4,11 @@
|
|||
<ul>
|
||||
<li>Encouraged by imperative paradigms.
|
||||
</li><li>Actions & mutable objects.
|
||||
</li><li>Time is <em>very</em> important: ex. linked list push
|
||||
</li><li>Time is <em>very</em> important<sup>*</sup>.
|
||||
</li><li>Synchronizing things is a challenge.
|
||||
</li>
|
||||
</ul>
|
||||
<p class="yellow">Natural Abstractions: pointers, variables, loop, Objects, Classes...</p>
|
||||
<p>Representation: a data structure changing other time.</p>
|
||||
|
||||
<p class="small">*: Push an element to a linked list for example</p>
|
|
@ -3,7 +3,7 @@
|
|||
<ul><li> Time is irrelevant by default.
|
||||
</li><li> Mostly static constructions like pipes.
|
||||
</li><li> All pipes can be plugged ⇒ all error at runtime
|
||||
<ul><li> (+ ("foo" 27) 32)
|
||||
<ul><li> (+ 37 "foo")
|
||||
</li><li> Y = λf.(λx.f (x x)) (λx.f (x x))
|
||||
</li><li> Y g = g (Y g)
|
||||
</li></ul>
|
|
@ -0,0 +1,6 @@
|
|||
<h2>Untyped Pure Programming</h2>
|
||||
|
||||
|
||||
<p style="text-align:center"><code>(+ 42 "foo")</code></p>
|
||||
|
||||
<img src="categories/img/mp/pipe.png" />
|
|
@ -43,7 +43,7 @@
|
|||
}
|
||||
</script>
|
||||
</head>
|
||||
<body id="body" class="deck-container" style="width: 99%">
|
||||
<body id="body" class="deck-container">
|
||||
|
||||
<div style="display:none">
|
||||
\(\newcommand{\F}{\mathbf{F}}\)
|
||||
|
|
|
@ -19,7 +19,6 @@ vardef hiddenoutmouth(expr pos) =
|
|||
enddef;
|
||||
def drawoutmouth(expr pos) =
|
||||
draw outmouth(pos);
|
||||
draw hiddenoutmouth(pos) dashed evely;
|
||||
enddef;
|
||||
|
||||
def drawtube(expr pos) =
|
||||
|
@ -48,11 +47,8 @@ enddef;
|
|||
def drawtwotubes(expr posintop,posinbot,posout) =
|
||||
begingroup;
|
||||
draw outmouth(posintop);
|
||||
draw hiddenoutmouth(posintop) dashed evenly;
|
||||
draw outmouth(posinbot);
|
||||
draw hiddenoutmouth(posinbot) dashed evenly;
|
||||
draw outmouth(posout);
|
||||
draw hiddenoutmouth(posout) dashed evenly;
|
||||
|
||||
save intopt,intopb,inbott,inbotb,outt,outb;
|
||||
pair intopt,intopb,inbott,inbotb,outt,outb;
|
||||
|
@ -74,16 +70,18 @@ def drawtwotubeslabel(expr ptop,pbot,pout,l) =
|
|||
drawtwotubes(ptop,pbot,pout);
|
||||
save mid;
|
||||
pair mid;
|
||||
mid = 1/4ptop+1/4pbot+1/2pout;
|
||||
mid = 6/30ptop+6/30pbot+18/30pout;
|
||||
label(l,mid);
|
||||
endgroup;
|
||||
enddef;
|
||||
def drawbegintube (expr pos) =
|
||||
draw (subpath (4,8) of fullcircle rotated -90) scaled 2u shifted pos shifted (-2u,0);
|
||||
draw (pos shifted (-2u,u)){right}..{right}(pos shifted (0,u));
|
||||
draw (pos shifted (-2u,-u)){right}..{right}(pos shifted (0,-u));
|
||||
def drawlongbegintube (expr pos,len) =
|
||||
draw (subpath (4,8) of fullcircle rotated -90) scaled 2u shifted pos shifted (-len,0);
|
||||
draw (pos shifted (-len,u)){right}..{right}(pos shifted (0,u));
|
||||
draw (pos shifted (-len,-u)){right}..{right}(pos shifted (0,-u));
|
||||
draw outmouth(pos);
|
||||
draw hiddenoutmouth(pos) dashed evenly;
|
||||
enddef;
|
||||
def drawbegintube (expr pos) =
|
||||
drawlongbegintube(pos,2u);
|
||||
enddef;
|
||||
|
||||
def drawbegintubelabel(expr pos,l) =
|
||||
|
@ -98,9 +96,7 @@ def drawtube(expr pos) =
|
|||
midin := pos;
|
||||
midout := pos shifted (gu,0);
|
||||
draw outmouth(midin);
|
||||
draw hiddenoutmouth(midin) dashed evenly;
|
||||
draw outmouth(midout);
|
||||
draw hiddenoutmouth(midout) dashed evenly;
|
||||
|
||||
save topin,topout,botin,botout;
|
||||
pair topin,topout,botin,botout;
|
||||
|
@ -118,14 +114,36 @@ def drawtubelabel(expr pos,l) =
|
|||
enddef;
|
||||
|
||||
pair pos;
|
||||
pos:=(gu,gu);
|
||||
drawbegintubelabel(pos shifted (-gu,.5gu),btex $37$ etex);
|
||||
drawbegintubelabel(pos shifted (-gu,-.5gu),btex $\mathtt{"foo"}$ etex);
|
||||
pos:=origin;
|
||||
z0=(2.5gu,.5gu);
|
||||
z1=(0,-1.5gu);
|
||||
z2=z1 shifted (3gu,0);
|
||||
|
||||
drawbegintubelabel(pos shifted (-.5gu,.5gu),btex $42$ etex);
|
||||
drawbegintubelabel(pos shifted (-.5gu,-.5gu),btex $\mathtt{"foo"}$ etex);
|
||||
drawtwotubeslabel(pos shifted (0,.5gu), pos shifted (0,-.5gu), pos shifted (gu,0),btex $+$ etex);
|
||||
draw inmouth(pos shifted (0,.5gu) );
|
||||
draw inmouth(pos shifted (0,-.5gu) );
|
||||
|
||||
z0=origin;
|
||||
drawbegintubelabel(z0,btex $37$ etex);
|
||||
drawbegintubelabel(z0 shifted (-2u,-gu),btex $\mathtt{"foo"}$ etex);
|
||||
drawoptions(withcolor green);
|
||||
drawbegintubelabel(z0,btex $42$ etex);
|
||||
drawtwotubeslabel(z0, z0 shifted (0,-gu), z0 shifted (gu,-0.5gu),btex $+$ etex);
|
||||
draw inmouth(z0 shifted (0,-gu));
|
||||
|
||||
drawtubelabel(z0 shifted (2gu,-.5gu),btex $37+$ etex);
|
||||
|
||||
drawoptions(withcolor green);
|
||||
drawbegintubelabel(z1,btex $\mathtt{"foo"}$ etex);
|
||||
drawtubelabel(z1,btex $\mathtt{(+\ 42)}$ etex)
|
||||
|
||||
drawoptions(withcolor red);
|
||||
drawlongbegintube(z2,5u);
|
||||
label(btex $\mathtt{(+\ 42\ "foo")}$ etex,z2 shifted (-3u,0));
|
||||
draw z2 shifted (-4u,2u) -- z2 shifted (0,-2u) dashed evenly withpen pencircle scaled 1bp;
|
||||
draw z2 shifted (-4u,-2u) -- z2 shifted (0,2u) dashed evenly withpen pencircle scaled 1bp;
|
||||
|
||||
drawoptions(withcolor base01);
|
||||
drawarrow pos shifted (gu+2u,0) -- pos shifted (gu+4u,0);
|
||||
drawarrow z0 shifted (-gu,-gu-u) .. z1 shifted (gu,2u);
|
||||
drawarrow pos shifted (gu+u,-1.5gu) -- pos shifted (gu+3u,-1.5gu);
|
||||
|
||||
|
|
Binary file not shown.
Before Width: | Height: | Size: 39 KiB After Width: | Height: | Size: 58 KiB |
|
@ -33,6 +33,10 @@
|
|||
font-weight: normal;
|
||||
font-style: normal; }
|
||||
|
||||
body.deck-container {
|
||||
width: 100%;
|
||||
padding: 0; }
|
||||
|
||||
.deck-container {
|
||||
font-family: "ComputerModernSansSerif", Helvetica, sans-serif;
|
||||
/* Header Numbering */ }
|
||||
|
@ -171,8 +175,10 @@
|
|||
.deck-container blockquote {
|
||||
font-style: italic;
|
||||
padding: 0 1em;
|
||||
border-left: solid 10px #586e75;
|
||||
color: #93a1a1; }
|
||||
border-left: solid 10px #586e75; }
|
||||
.deck-container blockquote em {
|
||||
font-style: normal;
|
||||
color: #93a1a1; }
|
||||
.deck-container blockquote ul {
|
||||
padding-left: 1.5em; }
|
||||
.deck-container abbr,
|
||||
|
@ -806,7 +812,11 @@
|
|||
margin-bottom: 1em; }
|
||||
.deck-container table {
|
||||
border: 1px solid #586e75;
|
||||
width: 100%; }
|
||||
width: 90%;
|
||||
margin: 1.5em auto;
|
||||
box-sizing: border-box;
|
||||
-moz-box-sizing: border-box;
|
||||
-webkit-box-sizing: border-box; }
|
||||
.deck-container table tr td {
|
||||
padding: 2px 0.5em; }
|
||||
.deck-container table tr:nth-child(odd) {
|
||||
|
@ -883,7 +893,7 @@
|
|||
font-size: 4em; } }
|
||||
@media only screen and (max-width: 1380px) {
|
||||
.deck-container {
|
||||
font-size: 2em; } }
|
||||
font-size: 2.5em; } }
|
||||
@media only screen and (max-width: 640px) {
|
||||
.deck-container {
|
||||
font-size: 1.5em; } }
|
||||
|
@ -920,6 +930,9 @@ body.deck-container {
|
|||
font-size: 0.5em; }
|
||||
.deck-container .deck-prev-link,
|
||||
.deck-container .deck-next-link {
|
||||
position: absolute;
|
||||
top: 90%;
|
||||
bottom: 1em;
|
||||
background-color: #073642;
|
||||
color: #586e75; }
|
||||
.deck-container .deck-prev-link:visited,
|
||||
|
|
|
@ -180,6 +180,10 @@ $secondTextColor: $base1
|
|||
color: $base02
|
||||
color: $base0
|
||||
|
||||
body.deck-container
|
||||
width: 100%
|
||||
padding: 0
|
||||
|
||||
.deck-container
|
||||
.base03
|
||||
color: $base03
|
||||
|
@ -335,7 +339,9 @@ $secondTextColor: $base1
|
|||
font-style: italic
|
||||
padding: 0 1em
|
||||
border-left: solid 10px $base01
|
||||
color: $base1
|
||||
em
|
||||
font-style: normal
|
||||
color: $base1
|
||||
ul
|
||||
padding-left: 1.5em
|
||||
|
||||
|
@ -1040,7 +1046,11 @@ $secondTextColor: $base1
|
|||
|
||||
table
|
||||
border: 1px solid $borderColor
|
||||
width: 100%
|
||||
width: 90%
|
||||
margin: 1.5em auto
|
||||
box-sizing: border-box
|
||||
-moz-box-sizing: border-box
|
||||
-webkit-box-sizing: border-box
|
||||
table tr td
|
||||
padding: 2px .5em
|
||||
table tr
|
||||
|
@ -1124,7 +1134,7 @@ $secondTextColor: $base1
|
|||
font-size: 4em
|
||||
@media only screen and (max-width: 1380px)
|
||||
.deck-container
|
||||
font-size: 2em
|
||||
font-size: 2.5em
|
||||
@media only screen and (max-width: 640px)
|
||||
.deck-container
|
||||
font-size: 1.5em
|
||||
|
@ -1164,6 +1174,9 @@ body.deck-container
|
|||
|
||||
.deck-prev-link,
|
||||
.deck-next-link
|
||||
position: absolute
|
||||
top: 90%
|
||||
bottom: 1em
|
||||
&:visited
|
||||
color: $base01
|
||||
&:hover
|
||||
|
|
Loading…
Reference in a new issue