From f5fc57d703339571f4725cb9a01a38d5aa19d588 Mon Sep 17 00:00:00 2001 From: "Yann Esposito (Yogsototh)" Date: Mon, 3 Dec 2012 22:30:31 +0100 Subject: [PATCH] updated --- categories.html | 33 +++++++------------ categories/10_Introduction/020_Plan.html | 1 - .../140_Untyped_Pure_Programming.html | 2 +- .../200_Type_Theory_Categories.html | 18 +++------- .../180_Monads_are_just_monoids_1_4.html | 12 +++---- .../30_How/180_Monads_are_just_monoids_1_4.md | 12 +++---- 6 files changed, 30 insertions(+), 48 deletions(-) diff --git a/categories.html b/categories.html index 3f10073..5bdba5d 100644 --- a/categories.html +++ b/categories.html @@ -92,7 +92,6 @@
  • General overview
  • Math & Abstraction
  • Programming & Abstraction
    • -
  • Categories & Abstraction
  • What?
    • @@ -317,7 +316,7 @@ Theory=(Axioms,StringsRules,
  • Y = λf.(λx.f (x x)) (λx.f (x x)) +
  • Y = λf.(λx.f (x x)) (λx.f (x x))
  • Y g = g (Y g)
    • @@ -391,19 +390,11 @@ type Product = Product {getProduct :: a} -- Just a named box
    -

    Type Theory ⇒ Categories

    - -
      -
    • Type theory helped to remove paradoxes in Set Theory.
      • -
    • Prevent relations between different kind of objects.
      • -
    • Used in computer science
      • -
    - -
      -
    • typed λ-calculus ⇒ cartesian closed categories
      • -
    • untyped λ-calculus ⇒ C-monoids (subclass of categories)
      • -
    • Martin-Löf type theories ⇒ locally cartesian closed categories
      • -
    +

    Type Theory & Categories

    +
    typed λ-calculus cartesian closed categories +
    untyped λ-calculus C-monoids (subclass of categories) +
    Martin-Löf type theories locally cartesian closed categories +

    Plan

    @@ -895,16 +886,16 @@ Haskell types is fractal:

    Monads are just monoids (1/4)

    -

    A monoid is a triplet \((E,∙,e)\) s.t.

    +

    A monoid is a triplet \((M,⊙,e)\) s.t.

      -
    • \(E\) a set
      • -
    • \(∙:E×E→E\)
      • -
    • \(e:1→E\)
      • +
    • \(M\) a set
      • +
    • \(⊙:E×E→M\)
      • +
    • \(e:1→M\)

    Satisfying

      -
    • \(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)
      • -
    • \(e∙x = x = x∙e, ∀x∈E\)
      • +
    • \(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\)
      • +
    • \(e⊙x = x = x⊙e, ∀x∈M\)
    diff --git a/categories/10_Introduction/020_Plan.html b/categories/10_Introduction/020_Plan.html index 2037f71..e2e41cc 100644 --- a/categories/10_Introduction/020_Plan.html +++ b/categories/10_Introduction/020_Plan.html @@ -5,7 +5,6 @@
  • General overview
  • Math & Abstraction
  • Programming & Abstraction
    • -
  • Categories & Abstraction
  • What?
    • diff --git a/categories/10_Introduction/140_Untyped_Pure_Programming.html b/categories/10_Introduction/140_Untyped_Pure_Programming.html index 596d638..20d6d20 100644 --- a/categories/10_Introduction/140_Untyped_Pure_Programming.html +++ b/categories/10_Introduction/140_Untyped_Pure_Programming.html @@ -4,7 +4,7 @@
  • Mostly static constructions like pipes.
  • All pipes can be plugged ⇒ all error at runtime
    • (+ 37 "foo") -
    • Y = λf.(λx.f (x x)) (λx.f (x x)) +
    • Y = λf.(λx.f (x x)) (λx.f (x x))
    • Y g = g (Y g)
    • diff --git a/categories/10_Introduction/200_Type_Theory_Categories.html b/categories/10_Introduction/200_Type_Theory_Categories.html index f21b2ac..5ed7049 100644 --- a/categories/10_Introduction/200_Type_Theory_Categories.html +++ b/categories/10_Introduction/200_Type_Theory_Categories.html @@ -1,13 +1,5 @@ -

    Type Theory ⇒ Categories

    - -
      -
    • Type theory helped to remove paradoxes in Set Theory.
      • -
    • Prevent relations between different kind of objects.
      • -
    • Used in computer science
      • -
    - -
      -
    • typed λ-calculus ⇒ cartesian closed categories
      • -
    • untyped λ-calculus ⇒ C-monoids (subclass of categories)
      • -
    • Martin-Löf type theories ⇒ locally cartesian closed categories
      • -
    +

    Type Theory & Categories

    +
    typed λ-calculus cartesian closed categories +
    untyped λ-calculus C-monoids (subclass of categories) +
    Martin-Löf type theories locally cartesian closed categories +
    diff --git a/categories/30_How/180_Monads_are_just_monoids_1_4.html b/categories/30_How/180_Monads_are_just_monoids_1_4.html index f561e6f..ab0d225 100644 --- a/categories/30_How/180_Monads_are_just_monoids_1_4.html +++ b/categories/30_How/180_Monads_are_just_monoids_1_4.html @@ -1,12 +1,12 @@

    Monads are just monoids (1/4)

    -

    A monoid is a triplet \((E,∙,e)\) s.t.

    +

    A monoid is a triplet \((M,⊙,e)\) s.t.

      -
    • \(E\) a set
      • -
    • \(∙:E×E→E\)
      • -
    • \(e:1→E\)
      • +
    • \(M\) a set
      • +
    • \(⊙:E×E→M\)
      • +
    • \(e:1→M\)

    Satisfying

      -
    • \(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)
      • -
    • \(e∙x = x = x∙e, ∀x∈E\)
      • +
    • \(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\)
      • +
    • \(e⊙x = x = x⊙e, ∀x∈M\)
    diff --git a/categories/30_How/180_Monads_are_just_monoids_1_4.md b/categories/30_How/180_Monads_are_just_monoids_1_4.md index 4a4b0b5..e456c23 100644 --- a/categories/30_How/180_Monads_are_just_monoids_1_4.md +++ b/categories/30_How/180_Monads_are_just_monoids_1_4.md @@ -1,13 +1,13 @@ Monads are just monoids (1/4) ----------------------------- -A monoid is a triplet \\((E,∙,e)\\) s.t. +A monoid is a triplet \\((M,⊙,e)\\) s.t. -- \\(E\\) a set -- \\(∙:E×E→E\\) -- \\(e:1→E\\) +- \\(M\\) a set +- \\(⊙:E×E→M\\) +- \\(e:1→M\\) Satisfying -- \\(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\\) -- \\(e∙x = x = x∙e, ∀x∈E\\) +- \\(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\\) +- \\(e⊙x = x = x⊙e, ∀x∈M\\)