#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)
5 Likes
The definition of natural transformation was wrong, the corrected version is as follows:
#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)
1 Like
;;; 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 ...) ...] ...}
;;; 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]))
#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))))
FSM actions as functors:
#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
#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)
#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
#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
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.
1 Like
#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)))
#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
CPS is a special case of Yoneda Lemma:
#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))
#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))
#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