revert to zsh version(s) back
This commit is contained in:
Yann Esposito (Yogsototh)
parent
f5fc57d703
commit
53f10e967c
6 changed files with 48 additions and 30 deletions
|
|
@ -92,6 +92,7 @@
|
|||
<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>
|
||||
</ul>
|
||||
</li>
|
||||
<li>What?</li>
|
||||
|
|
@ -316,7 +317,7 @@ Theory=(Axioms,<span style="visibility:hidden">Strings</span>Rules,<span style="
|
|||
</li><li> Mostly static constructions like pipes.
|
||||
</li><li> All pipes can be plugged ⇒ all error at runtime
|
||||
<ul><li> (+ 37 "foo")
|
||||
</li><li> Y = λf.(λx.f (x x)) (λx.f (<span class="yellow">x x</span>))
|
||||
</li><li> Y = λf.(λx.f (x x)) (λx.f (x x))
|
||||
</li><li> Y g = g (Y g)
|
||||
</li></ul>
|
||||
</li></ul>
|
||||
|
|
@ -390,11 +391,19 @@ type Product = Product {getProduct :: a} -- Just a named box
|
|||
|
||||
</section>
|
||||
<section class="slide">
|
||||
<h2>Type Theory <span class="and">&</span> Categories</h2>
|
||||
<table><tr><td>typed λ-calculus </td><td> cartesian closed categories
|
||||
</td></tr><tr><td>untyped λ-calculus </td><td> C-monoids (subclass of categories)
|
||||
</td></tr><tr><td>Martin-Löf type theories </td><td> locally cartesian closed categories
|
||||
</td></tr><tr><td></table>
|
||||
<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>Plan</h2>
|
||||
|
|
@ -886,16 +895,16 @@ Haskell types is fractal:</p>
|
|||
</section>
|
||||
<section class="slide">
|
||||
<h2 id="monads-are-just-monoids-14">Monads are just monoids (1/4)</h2>
|
||||
<p>A monoid is a triplet \((M,⊙,e)\) s.t.</p>
|
||||
<p>A monoid is a triplet \((E,∙,e)\) s.t.</p>
|
||||
<ul>
|
||||
<li>\(M\) a set</li>
|
||||
<li>\(⊙:E×E→M\)</li>
|
||||
<li>\(e:1→M\)</li>
|
||||
<li>\(E\) a set</li>
|
||||
<li>\(∙:E×E→E\)</li>
|
||||
<li>\(e:1→E\)</li>
|
||||
</ul>
|
||||
<p>Satisfying</p>
|
||||
<ul>
|
||||
<li>\(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\)</li>
|
||||
<li>\(e⊙x = x = x⊙e, ∀x∈M\)</li>
|
||||
<li>\(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)</li>
|
||||
<li>\(e∙x = x = x∙e, ∀x∈E\)</li>
|
||||
</ul>
|
||||
</section>
|
||||
<section class="slide">
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@
|
|||
<li class="yellow">General overview</li>
|
||||
<li>Math & Abstraction</li>
|
||||
<li>Programming & Abstraction</li>
|
||||
<li>Categories & Abstraction</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li>What?</li>
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
</li><li> Mostly static constructions like pipes.
|
||||
</li><li> All pipes can be plugged ⇒ all error at runtime
|
||||
<ul><li> (+ 37 "foo")
|
||||
</li><li> Y = λf.(λx.f (x x)) (λx.f (<span class="yellow">x x</span>))
|
||||
</li><li> Y = λf.(λx.f (x x)) (λx.f (x x))
|
||||
</li><li> Y g = g (Y g)
|
||||
</li></ul>
|
||||
</li></ul>
|
||||
|
|
|
|||
|
|
@ -1,5 +1,13 @@
|
|||
<h2>Type Theory & Categories</h2>
|
||||
<table><tr><td>typed λ-calculus </td><td> cartesian closed categories
|
||||
</td></tr><tr><td>untyped λ-calculus </td><td> C-monoids (subclass of categories)
|
||||
</td></tr><tr><td>Martin-Löf type theories </td><td> locally cartesian closed categories
|
||||
</td></tr><tr><td></table>
|
||||
<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>
|
||||
|
|
|
|||
|
|
@ -1,12 +1,12 @@
|
|||
<h2 id="monads-are-just-monoids-14">Monads are just monoids (1/4)</h2>
|
||||
<p>A monoid is a triplet \((M,⊙,e)\) s.t.</p>
|
||||
<p>A monoid is a triplet \((E,∙,e)\) s.t.</p>
|
||||
<ul>
|
||||
<li>\(M\) a set</li>
|
||||
<li>\(⊙:E×E→M\)</li>
|
||||
<li>\(e:1→M\)</li>
|
||||
<li>\(E\) a set</li>
|
||||
<li>\(∙:E×E→E\)</li>
|
||||
<li>\(e:1→E\)</li>
|
||||
</ul>
|
||||
<p>Satisfying</p>
|
||||
<ul>
|
||||
<li>\(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\)</li>
|
||||
<li>\(e⊙x = x = x⊙e, ∀x∈M\)</li>
|
||||
<li>\(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)</li>
|
||||
<li>\(e∙x = x = x∙e, ∀x∈E\)</li>
|
||||
</ul>
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
Monads are just monoids (1/4)
|
||||
-----------------------------
|
||||
|
||||
A monoid is a triplet \\((M,⊙,e)\\) s.t.
|
||||
A monoid is a triplet \\((E,∙,e)\\) s.t.
|
||||
|
||||
- \\(M\\) a set
|
||||
- \\(⊙:E×E→M\\)
|
||||
- \\(e:1→M\\)
|
||||
- \\(E\\) a set
|
||||
- \\(∙:E×E→E\\)
|
||||
- \\(e:1→E\\)
|
||||
|
||||
Satisfying
|
||||
|
||||
- \\(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\\)
|
||||
- \\(e⊙x = x = x⊙e, ∀x∈M\\)
|
||||
- \\(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\\)
|
||||
- \\(e∙x = x = x∙e, ∀x∈E\\)
|
||||
|
|
|
|||
Loading…
Reference in a new issue