#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)
3 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