# Functor, Natural tranformation, and Monad in Racket
**URL:** https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930
**Category:** Show & Tell
**Tags:** category
**Created:** [May 9, 2023, 7:04am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930 "2023-05-09T07:04:26Z")
**Posts on this page:** 15
**Page:** 1
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 9, 2023, 7:04am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/1 "2023-05-09T07:04:26Z")
```scheme
#lang racket
;; Functor F : (-> (-> A B) (-> (F A) (F B)))
;; f : (-> A B)
;; g : (-> B C)
#;(== (compose (F g) (F f))
(F (compose g f)))
;; Natural transformation α F->G : (-> (-> (F A) (F B)) (-> (F A) (G B)))
;; idA : (-> A A)
;; idB : (-> B B)
;; f : (-> A B)
#;(== (α (F f))
(compose (α (F idB)) (F f))
(compose (G f) (α (F idA))))
;; idC : (-> C C)
;; g : (-> B C)
#;(== (compose (α (F g)) (F f))
(compose (G g) (α (F f)))
(compose (α (F idC)) (F g) (F f))
(compose (G g) (α (F idB)) (F f))
(compose (G g) (G f) (α (F idA))))
;; List Monad
#;(== T
(compose μ η T)
(compose μ T η))
#;(== (compose μ T μ)
(compose μ μ T))
(define T (λ (f) (curry map f))) ; F = T
(define η (λ (f) (compose list f))) ; F = (compose), G = (compose T)
(define μ (λ (f) (compose append* f))) ; F = (compose T T), G = (compose T)
((η (compose)) 'a 'b 'c) ; '(a b c)
((μ (compose)) '((a) (b) (c))) ; '(a b c)
((μ (compose)) '((a b c))) ; '(a b c)
(((compose T η) (compose)) '(a b c)) ; '((a) (b) (c))
(((compose η T) (compose)) '(a b c)) ; '((a b c))
((T (compose)) '(a b c)) ; '(a b c)
(((compose μ T η) (compose)) '(a b c)) ; '(a b c)
(((compose μ η T) (compose)) '(a b c)) ; '(a b c)
(((compose T μ) (compose)) '(((a) (b) (c)) ((a b c)))) ; '((a b c) (a b c))
(((compose μ T) (compose)) '(((a) (b) (c)) ((a b c)))) ; '((a) (b) (c) (a b c))
(((compose μ T μ) (compose)) '(((a) (b) (c)) ((a b c)))) ; '(a b c a b c)
(((compose μ μ T) (compose)) '(((a) (b) (c)) ((a b c)))) ; '(a b c a b c)
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 16, 2023, 11:29am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/2 "2023-05-16T11:29:29Z")
The definition of natural transformation was wrong, the corrected version is as follows:
```scheme
#lang racket
(define ∘ compose)
(define ⋅
(let ([α->αid (λ (α) (α (∘)))])
(case-lambda
[() (∘)]
[(α) α]
[(α . α*)
(define αid (apply ∘ (map α->αid α*)))
(λ (f) (∘ (α f) αid))])))
;;; Functor F : (-> (-> A B) (-> (F A) (F B)))
;; f : (-> A B)
;; g : (-> B C)
#;(== (∘ (F g) (F f))
(F (∘ g f)))
;;; Natural transformation α : F => G : (-> (-> A B) (-> (F A) (G B)))
;; F = F.id : F => F : (-> (-> A B) (-> (F A) (F B)))
;; f : (-> A B)
#;(== (α f)
(∘ (α (∘)) (F f))
(∘ (G f) (α (∘))))
;; g : (-> B C)
#;(== (∘ (α g) (F f))
(∘ (G g) (α f))
(∘ (α (∘)) (F g) (F f))
(∘ (G g) (α (∘)) (F f))
(∘ (G g) (G f) (α (∘))))
;;; Monad T η μ
;; η : (∘) => T : (-> (-> A B) (-> A TB))
;; μ : (∘ T T) => T : (-> (-> A B) (-> TTA TB))
#;(== T T.id
(⋅ μ (∘ η T))
(⋅ μ (∘ T η)))
#;(== (⋅ μ (∘ T μ))
(⋅ μ (∘ μ T)))
;; List Monad
(define T (λ (f) (curry map f))) ; F = T
(define η (λ (f) (∘ list f))) ; F = (∘), G = T
(define μ (λ (f) (∘ append* (T (T f))))) ; F = (∘ T T), G = T
((η (∘)) 'a 'b 'c) ; '(a b c)
((μ (∘)) '((a) (b) (c))) ; '(a b c)
((μ (∘)) '((a b c))) ; '(a b c)
(((∘ T η) (∘)) '(a b c)) ; '((a) (b) (c))
(((∘ η T) (∘)) '(a b c)) ; '((a b c))
(((∘ T μ) (∘)) '(((a) (b) (c)) ((a b c)))) ; '((a b c) (a b c))
(((∘ μ T) (∘)) '(((a) (b) (c)) ((a b c)))) ; '((a) (b) (c) (a b c))
((T (∘)) '(a b c)) ; '(a b c)
(((⋅ μ (∘ η T)) (∘)) '(a b c)) ; '(a b c)
(((⋅ μ (∘ T η)) (∘)) '(a b c)) ; '(a b c)
(((⋅ μ (∘ T μ)) (∘)) '(((a) (b) (c)) ((a b c)))) ; '(a b c a b c)
(((⋅ μ (∘ μ T)) (∘)) '(((a) (b) (c)) ((a b c)))) ; '(a b c a b c)
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 17, 2023, 1:11am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/3 "2023-05-17T01:11:52Z")
```scheme
;;; Comonad L ϵ σ
;; ϵ : L => (∘) : (-> (-> A B) (-> LA B))
;; σ : L => (∘ L L) : (-> (-> A B) (-> LA LLB))
#;(== L L.id
(⋅ (∘ L ϵ) σ)
(⋅ (∘ ϵ L) σ))
#;(== (⋅ (∘ σ L) σ)
(⋅ (∘ L σ) σ))
;; Stream Comonad
(define (L f) (curry stream-map f)) ; F = L
(define (ϵ f) (∘ f stream-first)) ; F = L, G = (∘)
(define (σ f) (∘ (L (L f)) ; F = L, G = (∘ L L)
(λ (s)
(for/stream ([i (in-naturals)])
(stream-tail s i)))))
(define s (in-naturals)) ; (0 1 2 ...)
(define ss (stream-map in-naturals (in-naturals))) ; [(0 1 2 ...) (1 2 3 ...) ...]
((ϵ (∘)) s) ; 0
((σ (∘)) s) ; [(0 1 2 ...) (1 2 3 ...) ...]
(((∘ L ϵ) (∘)) ss) ; (0 1 2 ...)
(((∘ ϵ L) (∘)) ss) ; (0 1 2 ...)
(((∘ σ L) (∘)) ss) ; {[(0 1 2 ...) (1 2 3 ...) ...] [(1 2 3 ...) (2 3 4 ...) ...] ...}
(((∘ L σ) (∘)) ss) ; {[(0 1 2 ...) (1 2 3 ...) ...] [(1 2 3 ...) (2 3 4 ...) ...] ...}
((L (∘)) s) ; (0 1 2 ...)
(((⋅ (∘ L ϵ) σ) (∘)) s) ; (0 1 2 ...)
(((⋅ (∘ ϵ L) σ) (∘)) s) ; (0 1 2 ...)
(((⋅ (∘ σ L) σ) (∘)) s) ; {[(0 1 2 ...) (1 2 3 ...) ...] [(1 2 3 ...) (2 3 4 ...) ...] ...}
(((⋅ (∘ L σ) σ) (∘)) s) ; {[(0 1 2 ...) (1 2 3 ...) ...] [(1 2 3 ...) (2 3 4 ...) ...] ...}
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 17, 2023, 12:47pm UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/4 "2023-05-17T12:47:21Z")
```scheme
;;; Adjunct Functors F ⊣ G
;; η : (∘) => (∘ G F)
;; ϵ : (∘ F G) => (∘)
#;(== F F.id (⋅ (∘ ϵ F) (∘ F η)))
#;(== G G.id (⋅ (∘ G ϵ) (∘ η G)))
;; μ = (∘ G ϵ F) : (∘ G (∘ F G) F) => (∘ G (∘) F)
;; σ = (∘ F η G) : (∘ F (∘) G) => (∘ F (∘ G F) G)
;; T = (∘ G F)
;; L = (∘ F G)
;;;
;; (F A) == (Values A W)
;; (G A) == (-> W A)
;; F : (-> (-> A B) (-> (Values A W) (Values B W)))
;; G : (-> (-> A B) (-> (-> W A) (-> W B)))
;; η : (-> (-> A B) (-> A (-> W (Values B W))))
;; ϵ : (-> (-> A B) (-> (Values (-> W A) W) B))
(define (F f) (λ (a w) (values (f a) w)))
(define (G f) (λ (Ga) (λ (w) (call-with-values (λ () (Ga w)) f))))
(define (η f) #;(curry (F f)) (λ (a) (λ (w) (values (f a) w))))
(define (ϵ f) #;(uncurry (G f)) (λ (Ga w) (call-with-values (λ () (Ga w)) f)))
;; μ : (∘ T T) => T
;; σ : L => (∘ L L)
;; (T A) == (-> W (Values A W))
;; (L A) == (Values (-> W A) W)
(define μ (∘ G ϵ F))
(define σ (∘ F η G))
(define T (∘ G F))
(define L (∘ F G))
;;; State Monad T η μ
((η (∘)) 123) ; (λ (w) (values 123 w))
((μ (∘)) (λ (w) (values (λ (w) (values 123 w)) w))) ; (λ (w) (values 123 w))
(((∘ T η) (∘)) (λ (w) (values 123 w))) ; (λ (w) (values (λ (w) (values 123 w)) w))
(((∘ η T) (∘)) (λ (w) (values 123 w))) ; (λ (w) (values (λ (w) (values 123 w)) w))
(((∘ T μ) (∘)) (λ (w) (values (λ (w) (values (λ (w) (values 123 w)) w)) w))) ; (λ (w) (values (λ (w) (values 123 w)) w))
(((∘ μ T) (∘)) (λ (w) (values (λ (w) (values (λ (w) (values 123 w)) w)) w))) ; (λ (w) (values (λ (w) (values 123 w)) w))
((T (∘)) (λ (w) (values 123 w))) ; (λ (w) (values 123 w))
(((⋅ μ (∘ η T)) (∘)) (λ (w) (values 123 w))) ; (λ (w) (values 123 w))
(((⋅ μ (∘ T η)) (∘)) (λ (w) (values 123 w))) ; (λ (w) (values 123 w))
(((⋅ μ (∘ T μ)) (∘)) (λ (w) (values (λ (w) (values (λ (w) (values 123 w)) w)) w))) ; (λ (w) (values 123 w))
(((⋅ μ (∘ μ T)) (∘)) (λ (w) (values (λ (w) (values (λ (w) (values 123 w)) w)) w))) ; (λ (w) (values 123 w))
;;; Store Comonad L ϵ σ
((ϵ (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; 123
((σ (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; (values (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123]))
(((∘ L ϵ) (∘)) (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123])) ; (values (λ (w) (hash-ref w 'x)) #hash([x . 123]))
(((∘ ϵ L) (∘)) (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123])) ; (values (λ (w) (hash-ref w 'x)) #hash([x . 123]))
(((∘ σ L) (∘)) (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123])) ; (values (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123]))
(((∘ L σ) (∘)) (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123])) ; (values (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123]))
((L (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; (values (λ (w) (hash-ref w 'x)) #hash([x . 123]))
(((⋅ (∘ L ϵ) σ) (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; (values (λ (w) (hash-ref w 'x)) #hash([x . 123]))
(((⋅ (∘ ϵ L) σ) (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; (values (λ (w) (hash-ref w 'x)) #hash([x . 123]))
(((⋅ (∘ σ L) σ) (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; (values (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123]))
(((⋅ (∘ L σ) σ) (∘)) (λ (w) (hash-ref w 'x)) #hash([x . 123])) ; (values (λ (w) (values (λ (w) (hash-ref w 'x)) w)) #hash([x . 123]))
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 17, 2023, 8:19pm UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/5 "2023-05-17T20:19:17Z")
```scheme
#lang racket
;;; Morphism f : (->𝒞 A B)
#;(== f (∘𝒞 f id.A) (∘𝒞 id.B f))
;; g : (->𝒞 B C)
;; h : (->𝒞 C D)
#;(== (∘𝒞 h g f)
(∘𝒞 h (∘𝒞 g f))
(∘𝒞 (∘𝒞 h g) f))
(define (∘->· ∘)
;; ∘ : composition of morphisms
;; · : vertical composition of natural transofmations
;; compose : horizontal composition of natural transofmations
(define id (∘))
(define α->αid (λ (α) (α id)))
(case-lambda
[() values]
[(α) α]
[(α . α*)
(define αid (apply ∘ (map α->αid α*)))
(λ (f) (∘ (α f) αid))]))
;;; Category 𝒞
#;(== (->𝒞 A B) (-> A B))
(define ∘ compose)
(define · (∘->· ∘))
;; List Monad T η μ
(define (T f) (curry map f)) ; F = T
(define (η f) (∘ list f)) ; F = (∘), G = T
(define (μ f) (∘ append* (T (T f)))) ; F = (∘ T T), G = T
(define ηid (η (∘)))
(define μid (μ (∘)))
;;; Kleisli Category 𝒦(T) for List Monad
#;(== (->𝒦 ηA ηB) (-> A TB))
(define ∘𝒦
(case-lambda
[() ηid]
[(ηf) ηf]
[(ηg ηf)
(cond
[(eq? ηf ηid) ηg]
[(eq? ηg ηid) ηf]
[else (∘ (ϵ ηg) ηf)])]
[(ηf . ηf*) (∘𝒦 ηf (apply ∘𝒦 ηf*))]))
(define ·𝒦 (∘->· ∘𝒦))
;;; Adjunct Functor F ⊣ G
;; F : (-> (->𝒞 A B) (->𝒦 ηA ηB)) == (-> (-> A B) (-> A TB))
;; G : (-> (->𝒦 ηA ηB) (->𝒞 TA TB)) == (-> (-> A TB) (-> TA TB))
(define (ϵ ηf) (∘ μid (T ηf)))
(define F η)
(define G ϵ)
(define L (∘ F G))
(define σ (∘ F η G))
;;; Comonad L ϵ σ
;; L : (-> (->𝒦 ηA ηB) (->𝒦 LηA LηB)) == (-> (-> A TB) (-> TA TTB))
;; ϵ : (-> (->𝒦 ηA ηB) (->𝒦 LηA ηB)) == (-> (-> A TB) (-> TA TB))
;; σ : (-> (->𝒦 ηA ηB) (->𝒦 LηA LLηB)) == (-> (-> A TB) (-> TA TTTB))
((ϵ (∘𝒦)) '(a b c)) #;'(a b c)
((σ (∘𝒦)) '(a b c)) #;'(((a b c)))
(((∘ L ϵ) (∘𝒦)) '((a 0) (b 1) (c 2))) #;'((a 0 b 1 c 2))
(((∘ ϵ L) (∘𝒦)) '((a 0) (b 1) (c 2))) #;'((a 0) (b 1) (c 2))
(((∘ σ L) (∘𝒦)) '((a 0) (b 1) (c 2))) #;'((((a 0) (b 1) (c 2))))
(((∘ L σ) (∘𝒦)) '((a 0) (b 1) (c 2))) #;'((((a 0)) ((b 1)) ((c 2))))
((L (∘𝒦)) '(a b c)) #;'((a b c))
(((·𝒦 (∘ L ϵ) σ) (∘𝒦)) '(a b c)) #;'((a b c))
(((·𝒦 (∘ ϵ L) σ) (∘𝒦)) '(a b c)) #;'((a b c))
(((·𝒦 (∘ σ L) σ) (∘𝒦)) '(a b c)) #;'((((a b c))))
(((·𝒦 (∘ L σ) σ) (∘𝒦)) '(a b c)) #;'((((a b c))))
;;; T-algebras Category 𝒜𝓁ℊ(T) for List Monad
#;(== (->𝒜𝓁ℊ TA TB) (-> TA TB))
(define ∘𝒜𝓁ℊ (procedure-rename compose '∘𝒜𝓁ℊ))
(define ·𝒜𝓁ℊ (∘->· ∘𝒜𝓁ℊ))
;;; Adjunct Functor F ⊣ G
;; F : (-> (->𝒞 A B) (->𝒜𝓁ℊ TA TB)) == (-> (-> A B) (-> TA TB))
;; G : (-> (->𝒜𝓁ℊ TA TB) (->𝒞 TA TB)) == (-> (-> TA TB) (-> TA TB))
(define (ϵ Tf) (∘ μid (T Tf)))
(define F T)
(define G (∘))
(define L (∘ F G))
(define σ (∘ F η G))
;;; Comonad L ϵ σ
;; L : (-> (->𝒜𝓁ℊ TA TB) (->𝒜𝓁ℊ LTA LTB)) == (-> (-> TA TB) (-> TTA TTB))
;; ϵ : (-> (->𝒜𝓁ℊ TA TB) (->𝒜𝓁ℊ LTA TB)) == (-> (-> TA TB) (-> TTA TB))
;; σ : (-> (->𝒜𝓁ℊ TA TB) (->𝒜𝓁ℊ LTA LLTB)) == (-> (-> TA TB) (-> TTA TTTB))
((ϵ (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'(a b c 0 1 #t)
((σ (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'(((a b c)) ((0 1)) ((#t)))
(((∘ L ϵ) (∘𝒜𝓁ℊ)) '(((a b c) (0 1) (#t)) ((x y z) (9 8) (#f)))) #;'((a b c 0 1 #t) (x y z 9 8 #f))
(((∘ ϵ L) (∘𝒜𝓁ℊ)) '(((a b c) (0 1) (#t)) ((x y z) (9 8) (#f)))) #;'((a b c) (0 1) (#t) (x y z) (9 8) (#f))
(((∘ σ L) (∘𝒜𝓁ℊ)) '(((a b c) (0 1) (#t)) ((x y z) (9 8) (#f)))) #;'((((a b c) (0 1) (#t))) (((x y z) (9 8) (#f))))
(((∘ L σ) (∘𝒜𝓁ℊ)) '(((a b c) (0 1) (#t)) ((x y z) (9 8) (#f)))) #;'((((a b c)) ((0 1)) ((#t))) (((x y z)) ((9 8)) ((#f))))
((L (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'((a b c) (0 1) (#t))
(((·𝒜𝓁ℊ (∘ L ϵ) σ) (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'((a b c) (0 1) (#t))
(((·𝒜𝓁ℊ (∘ ϵ L) σ) (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'((a b c) (0 1) (#t))
(((·𝒜𝓁ℊ (∘ σ L) σ) (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'((((a b c))) (((0 1))) (((#t))))
(((·𝒜𝓁ℊ (∘ L σ) σ) (∘𝒜𝓁ℊ)) '((a b c) (0 1) (#t))) #;'((((a b c))) (((0 1))) (((#t))))
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 28, 2023, 2:15pm UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/6 "2023-05-28T14:15:46Z")
FSM actions as functors:
```scheme
#lang racket
(define state0 'start)
(define (string->char* str) (reverse (string->list str)))
(define transition
(let ([trl*
`([,state0 ,char-alphabetic? name]
[,state0 ,char-alphabetic? name]
[,state0 ,char-numeric? number]
[,state0 ,(curry char=? #\() lparen]
[,state0 ,(curry char=? #\)) rparen]
[name ,char-alphabetic? name]
[name ,char-numeric? name]
[number ,char-numeric? number])])
(λ (ch state)
(or
(for/or ([trl (in-list trl*)])
(match-define `[,s ,p? ,e] trl)
(and (symbol=? state s) (p? ch) e))
'error))))
(define (action ch* state)
(if (null? ch*)
state
(transition (car ch*) (action (cdr ch*) state))))
(define (recognizer str) (action (string->char* str) state0))
(for/list ([str (in-list '("abc112" "112" "(" ")"))]) (recognizer str)) ; '(name number lparen rparen)
(define ∘ compose)
(define ∘𝒞𝒽 append)
(define F (curry action))
;; input string: "abc112"
((F (∘𝒞𝒽 (string->char* "112") (string->char* "abc"))) state0) ; 'name
((∘ (F (string->char* "112")) (F (string->char* "abc"))) state0) ; 'name
;; input string: "112"
((F (∘𝒞𝒽 (string->char* "11") (string->char* "2"))) state0) ; 'number
((∘ (F (string->char* "11")) (F (string->char* "2"))) state0) ; 'number
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [May 31, 2023, 9:08am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/7 "2023-05-31T09:08:03Z")
```scheme
#lang racket
(define (∘->· ∘)
;; ∘ : composition of morphisms
;; · : vertical composition of natural transofmations
;; compose : horizontal composition of natural transofmations
(case-lambda
[() values]
[(α) α]
[(α . α*)
(λ (f)
(define id #;(domain f) (∘))
(define α->αid (λ (α) (α id)))
(define αid (apply ∘ (map α->αid α*)))
(∘ (α f) αid))]))
(define ∘ compose)
(define · (∘->· ∘))
;;; Reader Monad
;; T : (-> (-> A B) (-> (-> W A) (-> W B)))
;; η : (-> (-> A B) (-> A (-> W B)))
;; μ : (-> (-> A B) (-> (-> W (-> W A)) (-> W B)))
(define (reader a . w*) (for/list ([w (in-list w*)]) (hash-ref w a)))
(define (T f) (λ (Ta) (∘ f Ta)))
(define (η f) (λ (a) (λ (w) (f a))))
(define (μ f) (λ (TTa) (λ (w) (f ((TTa w) w)))))
((η (∘)) 0) #;(λ (_) 0)
((μ (∘)) (λ (w1) (λ (w2) (reader 'a w1 w2)))) #;(λ (w) (reader 'a w w))
(((∘ T η) (∘)) (λ (w) (reader 'a w))) #;(λ (w1) (λ (_) (reader 'a w1)))
(((∘ η T) (∘)) (λ (w) (reader 'a w))) #;(λ (_) (λ (w2) (reader 'a w2)))
(((∘ T μ) (∘)) (λ (w1) (λ (w2) (λ (w3) (reader 'a w1 w2 w3))))) #;(λ (w1) (λ (w2) (reader 'a w1 w2 w2)))
(((∘ μ T) (∘)) (λ (w1) (λ (w2) (λ (w3) (reader 'a w1 w2 w3))))) #;(λ (w1) (λ (w2) (reader 'a w1 w1 w2)))
((T (∘)) (λ (w) (reader 'a w))) #;(λ (w) (reader 'a w))
(((· μ (∘ η T)) (∘)) (λ (w) (reader 'a w))) #;(λ (w) (reader 'a w))
(((· μ (∘ T η)) (∘)) (λ (w) (reader 'a w))) #;(λ (w) (reader 'a w))
(((· μ (∘ T μ)) (∘)) (λ (w1) (λ (w2) (λ (w3) (reader 'a w1 w2 w3))))) #;(λ (w) (reader 'a w w w))
(((· μ (∘ μ T)) (∘)) (λ (w1) (λ (w2) (λ (w3) (reader 'a w1 w2 w3))))) #;(λ (w) (reader 'a w w w))
;;; Writer Comonad
;; L : (-> (-> A B) (-> (Values W A) (Values W B)))
;; ϵ : (-> (-> A B) (-> (Values W A) (Values B)))
;; σ : (-> (-> A B) (-> (Values W A) (Values W W B)))
(define w0 "Log0")
(define w1 "Log1")
(define w2 "Log2")
(define (L f) (λ (w . a) #;(values w (f a)) (call-with-values (λ () (apply f a)) (λ b (apply values w b)))))
(define (ϵ f) (λ (w . a) #;(values (f a)) (call-with-values (λ () (apply f a)) (λ b (apply values b)))))
(define (σ f) (λ (w . a) #;(values w w (f a)) (call-with-values (λ () (apply f a)) (λ b (apply values w w b)))))
((ϵ (∘)) w0 123) #;(values 123)
((σ (∘)) w0 123) #;(values w0 w0 123)
(((∘ L ϵ) (∘)) w1 w2 123) #;(values w1 123)
(((∘ ϵ L) (∘)) w1 w2 123) #;(values w2 123)
(((∘ σ L) (∘)) w1 w2 123) #;(values w1 w1 w2 123)
(((∘ L σ) (∘)) w1 w2 123) #;(values w1 w2 w2 123)
((L (∘)) w0 123) #;(values w0 123)
(((· (∘ L ϵ) σ) (∘)) w0 123) #;(values w0 123)
(((· (∘ ϵ L) σ) (∘)) w0 123) #;(values w0 123)
(((· (∘ σ L) σ) (∘)) w0 123) #;(values w0 w0 w0 123)
(((· (∘ L σ) σ) (∘)) w0 123) #;(values w0 w0 w0 123)
;;; L ⊣ T
;; State Monad: (∘ T L)
;; Store Comonad: (∘ L T)
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [June 3, 2023, 3:19am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/8 "2023-06-03T03:19:53Z")
```scheme
#lang typed/racket/base/no-check
(define ∘ compose)
(: id (-> Real Real))
(define (id n) (unless (real? n) (error)) n)
;; List Monad (T η μ)
(: T (-> (-> A B) (-> (Listof A) (Listof B))))
(: η (-> (-> A B) (-> A (Listof B))))
(: μ (-> (-> A B) (-> (Listof (Listof A)) (Listof B))))
(define (T f) (curry map f))
(define (η f) (∘ list f))
(define (μ f) (∘ append* (T (T f))))
;; A T-algebra Example: (id sum)
(: sum (-> (Listof Real) Real))
(define sum (curry apply +))
#;(== (∘ sum (μ id))
(∘ sum (T sum)))
#;(== id (∘ sum (η id)))
((η id) 6) ; '(6)
((μ id) '((1 2) (3))) ; '(1 2 3)
((T sum) '((1 2) (3))) ; '( 3 3)
((∘ sum (μ id)) '((1 2) (3))) ; 6
((∘ sum (T sum)) '((1 2) (3))) ; 6
(id 6) ; 6
((∘ sum (η id)) 6) ; 6
;; Stream Comonad (L ϵ σ)
(: L (-> (-> A B) (-> (Stream A) (Stream B))))
(: ϵ (-> (-> A B) (-> (Stream A) B)))
(: σ (-> (-> A B) (-> (Stream A) (Stream (Stream B)))))
(define (L f) (curry stream-map f))
(define (ϵ f) (∘ f stream-first))
(define (σ f) (∘ (L (L f))
(λ (s)
(for/stream ([i (in-naturals)])
(stream-tail s i)))))
;; A L-coalgebra Example: (id n->n*)
(: n->n* (-> Real (Stream Real)))
(define (n->n* n) (stream-cons n (n->n* n)))
#;(== (∘ (σ id) n->n*)
(∘ (L n->n*) n->n*))
#;(== id (∘ (ϵ id) n->n*))
((ϵ id) (in-naturals 0)) ; 0
((σ id) (in-naturals 0)) ; [(0 1 2 ...) (1 2 3 ...) ...]
((L n->n*) (in-naturals 0)) ; [(0 0 0 ...) (1 1 1 ...) ...]
((∘ (σ id) n->n*) 6) ; {[(6 6 6 ...) (6 6 6 ...) ...] [(6 6 6 ...) (6 6 6 ...) ...] ...}
((∘ (L n->n*) n->n*) 6) ; {[(6 6 6 ...) (6 6 6 ...) ...] [(6 6 6 ...) (6 6 6 ...) ...] ...}
(id 6) ; 6
((∘ (ϵ id) n->n*) 6) ; 6
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [June 4, 2023, 2:47am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/9 "2023-06-04T02:47:30Z")
```scheme
#lang typed/racket/no-check
;;; Category 𝒞 (∘ dom cod)
#;(== f
(∘ f)
(∘ f (dom f))
(∘ (cod f) f))
#;(== (∘ f g h)
(∘ f (∘ g h))
(∘ (∘ f g) h))
;;; Monoidal Category ℳ (𝒞 I ⊗ α λ ρ)
;; Rule 1. triangle identity
;; Rule 2. pentagon identity
#;(== I (⊗))
#;(== A (⊗ A))
(: ⊗ (case->
(-> (Values) (-> (⊗) (⊗)))
(-> (Values (-> A X)) (-> (⊗ A) (⊗ X)))
(-> (Values (-> A X) (-> B Y)) (-> (⊗ A B) (⊗ X Y)))))
(: α0 (-> (Values (-> A X) (-> B Y) (-> C Z)) (-> (⊗ A (⊗ B C)) (⊗ (⊗ X Y) Z))))
(: α1 (-> (Values (-> A X) (-> B Y) (-> C Z)) (-> (⊗ (⊗ A B) C) (⊗ X (⊗ Y Z)))))
(: λ0 (-> (-> A B) (-> (⊗ I A) B)))
(: λ1 (-> (-> A B) (-> A (⊗ I B))))
(: ρ0 (-> (-> A B) (-> (⊗ A I) B)))
(: ρ1 (-> (-> A B) (-> A (⊗ B I))))
;; A monoid object (T η μ) in Monoidal Category ℳ
;; Rule 1. associative law
;; Rule 2. left and right unit laws
(: id.T (-> (⊗ T) (⊗ T)))
(: η (-> (⊗) (⊗ T)))
(: μ (-> (⊗ T T) (⊗ T)))
;;; Braided Monoidal Category ℬ (ℳ β)
(: β0 (-> (Values (-> A X) (-> B Y)) (-> (⊗ A B) (⊗ Y X))))
(: β1 (-> (Values (-> A X) (-> B Y)) (-> (⊗ B A) (⊗ X Y))))
;;; Symmetric Monoidal Category 𝒮 (ℬ)
#;(== (⊗ f g)
(∘ (β0 g f) (β0 id.A id.B))
(∘ (β1 f g) (β1 id.B id.A))
(∘ (β0 id.Y id.X) (β0 f g))
(∘ (β1 id.X id.Y) (β1 g f)))
;;; Symmetric Monoidal Closed Category 𝒟 (𝒮)
;; For all A, (⊗ A _) has a right adjoint and (⊗ _ A) has a left adjoint
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [June 4, 2023, 5:05am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/10 "2023-06-04T05:05:27Z")
A monad is a monoid object in the monoidal category of endofunctors with the functor composition as the tensor product.
A semigroup with an identity element is a monoid object in the monoidal category of sets with the Cartesian product as the tensor product.
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [June 7, 2023, 2:48am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/11 "2023-06-07T02:48:11Z")
```scheme
#lang typed/racket/no-check
;; F ⊣ G
#;(== F (·𝒞->𝒟 (∘ ϵ F) (∘ F η)))
#;(== G (·𝒟->𝒞 (∘ G ϵ) (∘ η G)))
(: F (-> (->𝒞 a b) (->𝒟 Fa Fb)))
(: G (-> (->𝒟 x y) (->𝒞 Gx Gy)))
(: η (-> (->𝒞 a b) (->𝒞 a GFb)))
(: ϵ (-> (->𝒟 x y) (->𝒟 FGx y)))
;;; Universal Mapping Property
#;(== (η a) (∘𝒞 (G (F a)) (η a)))
#;(== (ϵ x) (∘𝒟 (ϵ x) (F (G x))))
(: f (->𝒞 a Gx))
(: g (->𝒟 Fa x))
#;(== f (∘𝒞 (G g) (η a)))
#;(== g (∘𝒟 (ϵ x) (F f)))
(: i (->𝒞 b a))
(: j (->𝒟 x y))
#;(== (∘𝒞 f i) (∘𝒞 (G g) (η i)))
#;(== (∘𝒟 j g) (∘𝒟 (ϵ j) (F f)))
;; Hom Functor
(: Hom-𝒞G (-> (Values (->𝒞 b a) (->𝒟 x y)) (-> (->𝒞 a Gx) (->𝒞 b Gy))))
(: Hom-F𝒟 (-> (Values (->𝒞 b a) (->𝒟 x y)) (-> (->𝒟 Fa x) (->𝒟 Fb y))))
(define (Hom-𝒞G i j) (λ (f) (∘𝒞 (G j) f i)))
(define (Hom-F𝒟 i j) (λ (g) (∘𝒟 j g (F i))))
;; Define Natural Isomorphism between Hom Functor by (co)unit
(: β (-> (Values (->𝒞 b a) (->𝒟 x y)) (-> (->𝒟 Fa x) (->𝒞 b Gy))))
(: γ (-> (Values (->𝒞 b a) (->𝒟 x y)) (-> (->𝒞 a Gx) (->𝒟 Fb y))))
(define (β i j) (λ (g) (∘𝒞 (G j) (G g) (η i))))
(define (γ i j) (λ (f) (∘𝒟 (ϵ j) (F f) (F i))))
;; Define (co)unit by Natural Isomorphism between Hom Functor
(: η (-> (->𝒞 a b) (->𝒞 a GFb)))
(: ϵ (-> (->𝒟 x y) (->𝒟 FGx y)))
(define (η f) ((β a (F b)) (F f)))
(define (ϵ g) ((γ (G x) y) (G g)))
#;(== g ((γ i j) ((β i j) g)))
#;(== f ((β i j) ((γ i j) f)))
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [June 13, 2023, 3:25am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/12 "2023-06-13T03:25:35Z")
```scheme
#lang typed/racket/no-check
(define ∘ compose)
;;; Hom Functor
(: Hom𝒞 (∀ (b a x y) (-> (Values (->𝒞 b a) (->𝒞 x y)) (-> (->𝒞 a x) (->𝒞 b y)))))
(define (Hom𝒞 i j) (λ (f) (∘𝒞 j f i)))
;;; Yoneda Embedding
(: Y0 (∀ (b a) (-> (->𝒞 b a) (∀ (x y) (-> (->𝒞 x y) (-> (->𝒞 a x) (->𝒞 b y)))))))
(: Y1 (∀ (x y) (-> (->𝒞 x y) (∀ (b a) (-> (->𝒞 b a) (-> (->𝒞 a x) (->𝒞 b y)))))))
(define Y0 (curry Hom𝒞))
(define Y1 (curryr Hom𝒞))
;;; Yoneda Lemma
(: id.a (∀ (a) (-> a a)))
(: id.x (∀ (x) (-> x x)))
(define (id.a a) a)
(define (id.x x) x)
(: Hom𝒞-a_ (∀ (x y) (-> (->𝒞 x y) (∀ (a) (-> (->𝒞 a x) (->𝒞 a y))))))
(: Hom𝒞-_x (∀ (b a) (-> (->𝒞 b a) (∀ (x) (-> (->𝒞 a x) (->𝒞 b x))))))
(define Hom𝒞-a_ (Y0 id.a))
(define Hom𝒞-_x (Y1 id.x))
(: F (∀ (x y) (-> (->𝒞 x y) (-> Fx Fy))))
(: Fa->α (∀ (a) (-> Fa (∀ (x y) (-> (->𝒞 x y) (-> (->𝒞 a x) Fy))))))
(: α->Fa (∀ (a) (-> (∀ (x y) (-> (->𝒞 x y) (-> (->𝒞 a x) Fy))) Fa)))
(define (Fa->α Fa) (λ (j) (λ (f) ((F (∘𝒞 j f)) Fa))))
(define (α->Fa α) ((α id.a) id.a))
(: G (∀ (b a) (-> (->𝒞 b a) (-> Ga Gb))))
(: Gx->β (∀ (x) (-> Gx (∀ (b a) (-> (->𝒞 b a) (-> (->𝒞 a x) Gb))))))
(: β->Gx (∀ (x) (-> (∀ (b a) (-> (->𝒞 b a) (-> (->𝒞 a x) Gb))) Gx)))
(define (Gx->β Gx) (λ (i) (λ (f) ((G (∘𝒞 f i)) Gx))))
(define (β->Gx β) ((β id.x) id.x))
;;; If F/G is a representable functor which is isomorphic to (Hom𝒞 id.a _)/(Hom𝒞 _ id.x),
;;; i.e. α/β is an isomorphism, then Fa/Gx is a universal element of F/G
;;; If Fa/Gx is a universal element of F/G, then F/G is a representable functor
;;; which is isomorphic to (Hom𝒞 id.a _)/(Hom𝒞 _ id.x), i.e. α/β is an isomorphism
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [June 13, 2023, 1:28pm UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/13 "2023-06-13T13:28:41Z")
CPS is a special case of Yoneda Lemma:
```scheme
#lang typed/racket/no-check
(define ∘ compose)
;;; Hom Functor
(: Hom (∀ (b a x y) (-> (Values (-> b a) (-> x y)) (-> (-> a x) (-> b y)))))
(define (Hom i j) (λ (f) (∘ j f i)))
;;; Yoneda Embedding
(: Y0 (∀ (b a) (-> (-> b a) (∀ (x y) (-> (-> x y) (-> (-> a x) (-> b y)))))))
(: Y1 (∀ (x y) (-> (-> x y) (∀ (b a) (-> (-> b a) (-> (-> a x) (-> b y)))))))
(define Y0 (curry Hom))
(define Y1 (curryr Hom))
;;; CPS
(: id.a (∀ (a) (-> a a)))
(define (id.a a) a)
(: reader (∀ (x y) (-> (-> x y) (∀ (a) (-> (-> a x) (-> a y))))))
(define reader (Y0 id.a))
(: F (∀ (x y) (-> (-> x y) (-> x y))))
(: a->α (∀ (a) (-> a (∀ (x y) (-> (-> x y) (-> (-> a x) y))))))
(: α->a (∀ (a) (-> (∀ (x y) (-> (-> x y) (-> (-> a x) y))) a)))
(define (F j) j)
(define (a->α a) (λ (j) (λ (f) ((F (∘ j f)) a))))
(define (α->a α) ((α id.a) id.a))
;; Yoneda Lemma shows that a ≅ (-> (-> a ans) ans),
;; so that f ≅ (cps (cps f)), so that f ≅ (cps f)
(: f (∀ (a b) (-> a b)))
(: (cps f) (∀ (a b ans) (-> (-> b ans) (-> a ans))))
(: (cps (cps f)) (∀ (a b ans) (-> (-> (-> a ans) ans) (-> (-> b ans) ans))))
(: cps (∀ (a b) (-> (-> a b) (∀ (ans) (-> (-> b ans) (-> a ans))))))
(: uncps (∀ (a b) (-> (∀ (ans) (-> (-> b ans) (-> a ans))) (-> a b))))
(define (cps f) (λ (k) (∘ k f)))
(define (uncps f) (f id.b))
;; examples
(: foo String)
(: fooCPS (∀ (ans) (-> (-> String ans) ans)))
(define foo "string")
(define fooCPS ((a->α foo) id.ans))
(: id.str (-> String String))
(: id.ans (∀ (ans) (-> ans ans)))
(define (id.str str) str)
(define (id.ans ans) ans)
;; foo ≅ fooCPS
#;(== foo (fooCPS id.str))
#;(== fooCPS ((a->α foo) id.ans))
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [July 12, 2023, 1:00pm UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/14 "2023-07-12T13:00:35Z")
```scheme
#lang typed/racket/no-check
(define ∘ compose)
(define ·
(case-lambda
[() values]
[(α) α]
[(α . α*)
(lambda (f)
(define id #;(domain f) (∘))
(define α->αid (lambda (α) (α id)))
(define αid (apply ∘ (map α->αid α*)))
(∘ (α f) αid))]))
(require data/maybe)
;; maybe monad T
(: T.η (∀ (a b) (-> (-> a b) (-> a (Maybe b)))))
(: T (∀ (a b) (-> (-> a b) (-> (Maybe a) (Maybe b)))))
(: T.μ (∀ (a b) (-> (-> a b) (-> (Maybe (Maybe a)) (Maybe b)))))
(define (T.η f) (lambda (a) (just (f a))))
(define (T f) (lambda (Ta) (match Ta [(nothing) nothing] [(just a) ((T.η f) a)])))
(define (T.μ f) (lambda (TTa) (match TTa [(nothing) nothing] [(just Ta) ((T f) Ta)])))
;; list monad S
(: S.η (∀ (a b) (-> (-> a b) (-> a (Listof b)))))
(: S (∀ (a b) (-> (-> a b) (-> (Listof a) (Listof b)))))
(: S.μ (∀ (a b) (-> (-> a b) (-> (Listof (Listof a)) (Listof b)))))
(define (S.η f) (∘ list f))
(define (S f) (curry map f))
(define (S.μ f) (∘ append* (S (S f))))
;;; Distributive Law
;; Let S and T be monads in the same category 𝒞,
;; a distributive law of T over S is a natural transformation λ : ST => TS.
#;(== (∘𝒞 T S.η) (·𝒞 λ (∘𝒞 S.η T )))
#;(== (∘𝒞 T.η S) (·𝒞 λ (∘𝒞 S T.η)))
#;(== (·𝒞 (∘𝒞 T S.μ) (∘𝒞 λ S) (∘𝒞 S λ)) (·𝒞 λ (∘𝒞 S.μ T)))
#;(== (·𝒞 (∘𝒞 T.μ S) (∘𝒞 T λ) (∘𝒞 λ T)) (·𝒞 λ (∘𝒞 S T.μ)))
(: λ (∀ (a b) (-> (-> a b) (-> (Listof (Maybe a)) (Maybe (Listof b))))))
(define (λ f)
(lambda (STa)
(if (ormap nothing? STa)
nothing
(just (map (∘ f from-just!) STa)))))
(((∘ T S.η) (∘)) (nothing)) #;(nothing)
(((∘ T S.η) (∘)) (just 10)) #;(just (list 10))
(((· λ (∘ S.η T)) (∘)) (nothing)) #;(nothing)
(((· λ (∘ S.η T)) (∘)) (just 10)) #;(just (list 10))
(((∘ T.η S) (∘)) (list 10)) #;(just (list 10))
(((· λ (∘ S T.η)) (∘)) (list 10)) #;(just (list 10))
(((· (∘ T S.μ) (∘ λ S) (∘ S λ)) (∘)) (list (list (nothing)))) #;(nothing)
(((· (∘ T S.μ) (∘ λ S) (∘ S λ)) (∘)) (list (list (just 10)))) #;(just (list 10))
(((· (∘ T S.μ) (∘ λ S) (∘ S λ)) (∘)) (list (list (nothing) (just 10)))) #;(nothing)
(((· λ (∘ S.μ T)) (∘)) (list (list (nothing)))) #;(nothing)
(((· λ (∘ S.μ T)) (∘)) (list (list (just 10)))) #;(just (list 10))
(((· λ (∘ S.μ T)) (∘)) (list (list (nothing) (just 10)))) #;(nothing)
(((· (∘ T.μ S) (∘ T λ) (∘ λ T)) (∘)) (list (just (just 10)))) #;(just (list 10))
(((· (∘ T.μ S) (∘ T λ) (∘ λ T)) (∘)) (list (just (nothing)))) #;(nothing)
(((· (∘ T.μ S) (∘ T λ) (∘ λ T)) (∘)) (list (nothing))) #;(nothing)
(((· λ (∘ S T.μ)) (∘)) (list (just (just 10)))) #;(just (list 10))
(((· λ (∘ S T.μ)) (∘)) (list (just (nothing)))) #;(nothing)
(((· λ (∘ S T.μ)) (∘)) (list (nothing))) #;(nothing)
;; TS becomes a monad (ST doesn't).
(: TS.η (∀ (a b) (-> (-> a b) (-> a (Maybe (Listof b))))))
(: TS (∀ (a b) (-> (-> a b) (-> (Maybe (Listof a)) (Maybe (Listof b))))))
(: TS.μ (∀ (a b) (-> (-> a b) (-> (Maybe (Listof (Maybe (Listof a)))) (Maybe (Listof b))))))
(define TS.η (∘ T.η S.η))
(define TS (∘ T S ))
(define TS.μ (· (∘ T.μ S.μ) (∘ T λ S)))
;; if (∘𝒞 T S.η) and (∘𝒞 T.η S) are monad maps,
;; and the middle unitary law holds,
;; then we can define distributive law λ by TS monad.
#;(== (·𝒞 TS.μ (∘𝒞 T S.η T.η S )) (∘ T S)) ; middle unitary law
#;(== (·𝒞 TS.μ (∘𝒞 T.η S T S.η)) λ) ; define λ by TS monad
(: r (-> Real Real)) ; identity morphism of Real
(: t (-> (Maybe Real) Real)) ; a T-algebra
(: s (-> (Listof Real) Real)) ; a S-algebra
(: ts (-> (Maybe (Listof Real)) Real)) ; a TS-algebra
(: st (-> (Listof (Maybe Real)) Real)) ; not an algebra, because ST isn't a monad
(define r (∘))
;; define ts, st by t and s.
(define t0 (curry from-just +nan.0))
(define s0 (curry apply +))
(define ts0 (∘ t0 (T s0)))
(define st0 (∘ s0 (S t0)))
;; define st, t and s by ts.
(define ts1 (lambda (TSr) (match TSr [(nothing) +nan.0] [(just Sr) (apply + Sr)])))
(define st1 (∘ ts1 (λ r)))
(define t1 (∘ ts1 (T (S.η r))))
(define s1 (∘ ts1 (T.η (S r))))
#;(and (== t0 t1) (== s0 s1) (== ts0 ts1) (== st0 st1))
```
---
### Author:  [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)
#### Post date: [August 4, 2023, 6:06am UTC](https://racket.discourse.group/t/functor-natural-tranformation-and-monad-in-racket/1930/15 "2023-08-04T06:06:21Z")
```scheme
#lang typed/racket/no-check
;;;; Higher Category
;; Higher category is very useful for discussing some abstract concepts,
;; for example, 2-categories provide the context for discussing adjunctions and monads.
;;; 0-Category
;; A 0-category (set) consists of 0-cells (elements),
;; Each type `T` can be regard as a 0-category `𝒞`,
;; each value `t` of `T` can be regard as a 0-cell `c` of `𝒞`.
#;(: c ( >𝒞))
;;; 1-Category
;; A 1-category (category) consists of 0-cells (objects) and 1-cells (morphisms),
;; since for any object, there is a unique identity morphism corresponding to it one-to-one,
;; we can regard objects as special morphisms (identity morphisms).
;; So that we can abstract a 1-category into operators dealing with 1-cells,
;; in other words (1-dom𝒞 1-cod𝒞 1-∘𝒞) constructs a 1-category 𝒞.
#;(: a ( >𝒞))
#;(: b ( >𝒞))
#;(: F (->𝒞 a b))
#;(: id.a (->𝒞 a a))
#;(: id.b (->𝒞 b b))
#;(== (1-dom𝒞 F) id.a)
#;(== (1-cod𝒞 F) id.b)
#;(== F
(1-∘𝒞 F)
(1-∘𝒞 F id.a)
(1-∘𝒞 id.b F))
#;(: G (->𝒞 b c))
#;(: H (->𝒞 c d))
#;(== (1-∘𝒞 H G F)
(1-∘𝒞 H (1-∘𝒞 G F))
(1-∘𝒞 (1-∘𝒞 H G) F))
;;; 2-Category
;; A 2-category consists of 0-cells, 1-cells and 2-cells,
;; since for any 1-cell, there is a unique identity 2-cell corresponding to it one-to-one,
;; and for any 0-cell, there is a unique identity 1-cell corresponding to it one-to-one,
;; we can regard 0-cells and 1-cells as special 2-cells.
;; So that we can abstract a 2-category into operators dealing with 2-cells,
;; in other words (1-dom𝒞 1-cod𝒞 1-∘𝒞 2-dom𝒞 2-cod𝒞 2-∘𝒞) constructs a 2-category 𝒞.
;; A 2-category 𝒞 has 3 1-category structures on it:
;; 1. base category (1-dom𝒞 1-cod𝒞 1-∘𝒞): 0-cells as objects, 1-cells as morphisms
;; 2. horizontal category (1-dom𝒞 1-cod𝒞 1-∘𝒞): 0-cells as objects, 2-cells as morphisms
;; 3. vertical category (2-dom𝒞 2-cod𝒞 2-∘𝒞): 1-cells as objects, 2-cells as morphisms
#;(: a ( >𝒞))
#;(: b ( >𝒞))
#;(: F1 (->𝒞 a b))
#;(: F2 (->𝒞 a b))
#;(: id.a (->𝒞 a a))
#;(: id.b (->𝒞 b b))
#;(: α (=>𝒞 F1 F2))
#;(: id.F1 (=>𝒞 F1 F1))
#;(: id.F2 (=>𝒞 F2 F2))
#;(== (2-dom𝒞 α) id.F1)
#;(== (2-cod𝒞 α) id.F2)
#;(== α
(2-∘𝒞 α)
(2-∘𝒞 α id.F1)
(2-∘𝒞 id.F2 α))
#;(: α (=>𝒞 F1 F2))
#;(: β (=>𝒞 F2 F3))
#;(: (2-∘𝒞 β α) (=>𝒞 F1 F3)) ; vertical composition of 2-cells
#;(: id.id.a (=>𝒞 id.a id.a))
#;(: id.id.b (=>𝒞 id.b id.b))
#;(== (1-dom𝒞 α) id.id.a)
#;(== (1-cod𝒞 α) id.id.b)
#;(== α
(1-∘𝒞 α)
(1-∘𝒞 α id.id.a)
(1-∘𝒞 id.id.b α))
#;(: c ( >𝒞))
#;(: G1 (->𝒞 b c))
#;(: G2 (->𝒞 b c))
#;(: (1-∘𝒞 G1 F1) (->𝒞 a c)) ; base composition of 1-cells
#;(: (1-∘𝒞 G2 F2) (->𝒞 a c))
#;(: α (=>𝒞 F1 F2))
#;(: γ (=>𝒞 G1 G2))
#;(: (1-∘𝒞 γ α) (=>𝒞 (1-∘𝒞 G1 F1) (1-∘𝒞 G2 F2))) ; horizontal composition of 2-cells
```