The Yoneda Lemma

; The hom-functor Hom(a, -) is the Reader functor.
; Reader a x = a -> x
; fmap f h = f . h   (post-compose)

(define (reader-fmap f h)
  (lambda (a) (f (h a))))

; Fix a = Int. Hom(Int, -) maps every type x
; to the set of functions Int -> x.
(define (square x) (* x x))
(define (show-int n) (string-append "val=" (number->string n)))

; fmap show-int over square : Int -> Int becomes Int -> String
(define square-then-show (reader-fmap show-int square))

(display (square-then-show 5)) (newline)
; "val=25" — post-compose show-int after square

(display (square-then-show 3))
; "val=9"

; The Yoneda bijection:
;   phi : (forall x . (a -> x) -> F x) -> F a
;   phi alpha = alpha id
;
;   psi : F a -> (forall x . (a -> x) -> F x)
;   psi fa h = fmap h fa

; -- Direction 1: phi extracts the element at id --
(define (phi alpha)
  (alpha (lambda (x) x)))   ; apply alpha to id_a

; -- Direction 2: psi rebuilds alpha from a single element --
; For lists: fmap = map
(define (psi-list fa h)
  (map h fa))

; Start with a list fa = (1 2 3) in F(Int) where F = List
(define fa '(1 2 3))

; Build a natural transformation from this single element
(define (alpha-from-fa h) (psi-list fa h))

; Apply it to various functions (a -> x):
(display "alpha id:     ") (display (alpha-from-fa (lambda (x) x))) (newline)
(display "alpha square: ") (display (alpha-from-fa (lambda (x) (* x x)))) (newline)
(display "alpha show:   ") (display (alpha-from-fa number->string)) (newline)

; Round-trip: phi(alpha-from-fa) should give back fa
(display "phi recovers: ") (display (phi alpha-from-fa))
; (1 2 3) — the original element

; The proof: naturality pins down every component from id_a.
;
; Naturality square at f : a -> y :
;   alpha_y (f . id_a) = (fmap f) (alpha_a id_a)
;   alpha_y f           = fmap f seed
;
; where seed = alpha_a(id_a)

; For Maybe: fmap f Nothing = Nothing, fmap f (Just x) = Just (f x)
(define nothing (cons 'nothing '()))
(define (just x) (cons 'just x))
(define (nothing? m) (eq? (car m) 'nothing))

(define (fmap-maybe f m)
  (if (nothing? m) nothing (just (f (cdr m)))))

; Seed = Just(7). This single value determines the entire nat. trans.
(define seed (just 7))

; alpha_x(h) = fmap h seed, for any h : Int -> x
(define (alpha-maybe h)
  (fmap-maybe h seed))

(display "alpha id:     ") (display (alpha-maybe (lambda (x) x))) (newline)
(display "alpha (*2):   ") (display (alpha-maybe (lambda (x) (* x 2)))) (newline)
(display "alpha show:   ") (display (alpha-maybe number->string)) (newline)

; Seed = Nothing. A different element of F(a) = Maybe(Int).
(define seed2 nothing)
(define (alpha2 h) (fmap-maybe h seed2))

(display "alpha2 id:    ") (display (alpha2 (lambda (x) x))) (newline)
(display "alpha2 (*2):  ") (display (alpha2 (lambda (x) (* x 2))))
; Nothing everywhere — naturality propagates the Nothing.

; length : List a -> Int is a natural transformation.
; Naturality: length (map f xs) = length xs
; It never inspects the elements, only the structure.

(define (my-length lst)
  (if (null? lst) 0 (+ 1 (my-length (cdr lst)))))

; Check naturality: length . fmap f = length
(define xs '(10 20 30 40))

(display "length xs:             ")
(display (my-length xs)) (newline)

(display "length (map square xs): ")
(display (my-length (map (lambda (x) (* x x)) xs))) (newline)

(display "length (map show xs):   ")
(display (my-length (map number->string xs))) (newline)

; All 4. The natural transformation doesn't care what f does.
; This is the naturality condition in action:
; Const(length) . fmap f = id . Const(length)

; Yoneda embedding: a |-> Hom(a, -)
; Nat(Hom(a, -), Hom(b, -)) = Hom(b, a)
;
; Every nat trans between hom-functors is pre-composition
; with a morphism g : b -> a.

; In types: (forall x . (a -> x) -> (b -> x)) ≅ (b -> a)
; alpha h = h . g   (pre-compose with g)

; g : String -> Int (the morphism b -> a)
(define (g s) (string-length s))

; The nat trans: for any h : Int -> x, produce String -> x
(define (alpha h)
  (lambda (s) (h (g s))))

; Test at different h:
(define (double x) (* x 2))
(define (is-big x) (> x 5))

(display "alpha(double)("hello"): ")
(display ((alpha double) "hello")) (newline)
; string-length "hello" = 5, double 5 = 10

(display "alpha(is-big)("hi"):    ")
(display ((alpha is-big) "hi")) (newline)
; string-length "hi" = 2, is-big 2 = #f

; Recover g from alpha: apply to id
(display "phi(alpha)("hello"):    ")
(display ((alpha (lambda (x) x)) "hello"))
; 5 — that's g("hello") = string-length "hello"

; Co-Yoneda: the contravariant version.
; Nat(Hom(-, a), F) ≅ F(a)  for contravariant F
;
; In programming terms:
;   (forall x . (x -> a) -> F x) ≅ F a
;
; phi alpha = alpha id
; psi fa h  = contramap h fa

; Predicate as a contravariant functor:
; contramap : (x -> a) -> Pred(a) -> Pred(x)
(define (contramap-pred f pred)
  (lambda (x) (pred (f x))))

; A predicate on Int: is it positive?
(define (positive? n) (> n 0))

; Co-Yoneda: psi turns a predicate into a nat trans
(define (psi-pred pred h)
  (contramap-pred h pred))

; This nat trans works for any h : x -> Int
(define (str-len s) (string-length s))

(define positive-length? (psi-pred positive? str-len))

(display "positive-length?("hello"): ")
(display (positive-length? "hello")) (newline)
; string-length "hello" = 5, positive? 5 = #t

(display "positive-length?(""): ")
(display (positive-length? "")) (newline)
; string-length "" = 0, positive? 0 = #f

; Round-trip: phi recovers the original predicate
(define recovered (psi-pred positive? (lambda (x) x)))
(display "recovered(3):  ") (display (recovered 3)) (newline)
(display "recovered(-1): ") (display (recovered -1))

; CPS is Yoneda with F = Identity.
; (forall x . (a -> x) -> x) ≅ a
;
; "Having a value" = "being able to hand it to any continuation"

; Wrap a value in CPS: a -> (forall x . (a -> x) -> x)
(define (to-cps val)
  (lambda (k) (k val)))

; Unwrap: apply to id
(define (from-cps cps-val)
  (cps-val (lambda (x) x)))

; Round-trip
(define cps-42 (to-cps 42))

(display "from-cps: ") (display (from-cps cps-42)) (newline)
; 42

; The CPS value responds to any continuation:
(display "double:   ") (display (cps-42 (lambda (x) (* x 2)))) (newline)
(display "show:     ") (display (cps-42 number->string)) (newline)
(display "is-big:   ") (display (cps-42 (lambda (x) (> x 10))))
; The value 42 is "inside" — you access it only through continuations.