Kleisli.lean

View source on GitHub

Kernel

A Kernel is a function from a to M b — given an input, it produces a computation that may be stochastic. When M = Id, this is just a plain function a → b. Every pipeline stage is a Kernel. This is the Kleisli arrow that the formal backbone uses to model morphisms in the Stoch category.

def Kernel (M : Type → Type) (α β : Type) := α → M β

Kernel.comp

Kleisli composition: feed the output of the first kernel into the second, chaining via bind. This is how pipeline stages connect — the output of Perceive flows into Cache, Cache into Filter, and so on.

def Kernel.comp [Monad M] (f : Kernel M α β) (g : Kernel M β γ)
    : Kernel M α γ :=
  fun a => f a >>= g

Kernel.id_comp / comp_id / comp_assoc

The three category laws: composing with the identity kernel does nothing (left and right), and composition is associative. All three follow from the monad laws — this is the standard result that every lawful monad induces a Kleisli category.

theorem Kernel.comp_assoc [Monad M] [LawfulMonad M]
    (f : Kernel M α β) (g : Kernel M β γ) (h : Kernel M γ δ)
    : Kernel.comp (Kernel.comp f g) h =
      Kernel.comp f (Kernel.comp g h)

The proof uses funext (two functions are equal if they agree on all inputs) and then applies bind_assoc from the LawfulMonad instance.

; Kleisli composition: chain functions that return lists
; a -> [b], b -> [c]  =>  a -> [c]
; (like composing stochastic stages)

(define (kleisli-comp f g)
  (lambda (x)
    (apply append (map g (f x)))))

; Stage 1: perceive — one input, two encodings
(define (perceive x)
  (list (string-append x "-visual")
        (string-append x "-audio")))

; Stage 2: cache — each encoding gets indexed
(define (cache enc)
  (list (string-append enc ":idx0")
        (string-append enc ":idx1")))

; Compose: perceive >=> cache
(define pipeline (kleisli-comp perceive cache))

(display "perceive('cat'): ")
(display (perceive "cat"))
(newline)
(display "pipeline('cat'): ")
(display (pipeline "cat"))

# Kleisli composition: chain functions that return lists
# a -> [b], b -> [c]  =>  a -> [c]
# (like composing stochastic stages)

def kleisli_comp(f, g):
    return lambda x: [z for y in f(x) for z in g(y)]

# Stage 1: perceive — one input, two encodings
def perceive(x):
    return [x + "-visual", x + "-audio"]

# Stage 2: cache — each encoding gets indexed
def cache(enc):
    return [enc + ":idx0", enc + ":idx1"]

# Compose: perceive >=> cache
pipeline = kleisli_comp(perceive, cache)

print(f"perceive('cat'): {perceive('cat')}")
print(f"pipeline('cat'): {pipeline('cat')}")

Kernel.deterministic_comp

Pure functions can be embedded as kernels (wrap the output in pure). This embedding preserves composition: embedding g . f gives the same kernel as composing the embeddings of f and g separately.

theorem Kernel.deterministic_comp [Monad M] [LawfulMonad M]
    (f : α → β) (g : β → γ)
    : Kernel.deterministic (M := M) (g ∘ f) =
      Kernel.comp (Kernel.deterministic f) (Kernel.deterministic g)

Connections

• Support.lean — imported; kernels compose over the possibilistic layer
• Pipeline.lean — the pipeline is built from five forward kernels + one backward kernel
• Contracts.lean — contract preservation is defined on kernels