Chapter 4: Theoretical Robustness — Re-examining the Functor/Monad Laws

In the previous chapters, we have looked at two main APIs: .map() and .bind(). This chapter will prove that these operations are not just a collection of convenient features, but are built on a mathematically robust foundation.

Why Are “Laws” Important? (Revisited)

First, let’s briefly review the Functor/Monad laws discussed in Unit 2. Why is the verification of such abstract “laws” important?

It is because by satisfying these laws, the behavior of the API becomes predictable, allowing developers to combine and refactor code with confidence. This is not only for human development but also serves as an absolute foundation for AI to automatically generate and refactor code, producing robust, maintainable code that is free of logical flaws and bugs.

Re-examining the Functor Laws (.map)

The Functor laws ensure that .map() correctly “preserves” the fundamental structure of function composition.

1. Identity: timeline.map(id) is equivalent in behavior to timeline.
2. Composition: timeline.map(f).map(g) is equivalent in behavior to timeline.map(g << f).

// Identity function
const id = <A>(x: A): A => x;

// Functions to compose
const f_functor = (x: number): string => `value: ${x}`;
const g_functor = (s: string): boolean => s.length > 10;

const initialTimeline_functor = Timeline(5);

// 1. Verifying the Identity Law
const mappedById = initialTimeline_functor.map(id);
// initialTimeline_functor.at(Now) is 5
// mappedById.at(Now) is also id(5) = 5, and their behaviors are equivalent

// 2. Verifying the Composition Law
const composedFunc = (x: number) => g_functor(f_functor(x));
const result_LHS = initialTimeline_functor.map(composedFunc); // g(f(5)) -> false
const result_RHS = initialTimeline_functor.map(f_functor).map(g_functor);   // f(5) -> "value: 5" -> g("value: 5") -> false

// Both are equivalent in behavior

Re-examining the Monad Laws (.bind)

The verification of the Monad laws is done using the simpler and more essential approach of Kleisli composition. This is equivalent to verifying that the composition operator >>> for functions that return a Timeline (Kleisli arrows) forms a Monoid with ID as the identity element.

Definitions

• Kleisli Arrow: A function with the signature 'a -> Timeline<'b>.

• Identity Element (ID): A function that wraps a value in a Timeline.

• Kleisli Composition (>>>): An operator that connects two Kleisli arrows with .bind(). f >>> g is defined as x => f(x).bind(g).

Verifying the Monoid Laws

1. Associativity

• Law: (f >>> g) >>> h is equivalent to f >>> (g >>> h).
  • Explanation of Inevitability: This law is directly guaranteed by the associativity of .bind() itself: m.bind(f).bind(g) is equivalent to m.bind(x => f(x).bind(g)). DependencyCore does not care how you “group” your dependency definitions. Whether you define it in steps A→B→C or as a single continuous rule A→C, the final information flow path constructed is exactly the same. The associativity law is the mathematical expression of this self-evident principle in the dependency graph model: “the method of defining dependencies does not affect the final flow of information.”

2. Left Identity

• Law: ID >>> f is equivalent to f.
  • Explanation of Inevitability: Applying ID >>> f to a value a results in ID(a).bind(f), which is equivalent to f(a). The Timeline ID(a) is merely a temporary wrapper to kick off the next computation f, and it is self-evident that their behaviors are equivalent.

3. Right Identity

• Law: f >>> ID is equivalent to f.
  • Explanation of Inevitability: Applying f >>> ID to a value a results in f(a).bind(ID), which is equivalent to f(a). This is because the operation .bind(ID) is the same as passing the value from f(a) downstream without doing anything.

Verification with Code

// --- Definitions ---
const ID = <A>(x: A): Timeline<A> => Timeline(x);

const kleisliCompose = <A, B, C>(f: (a: A) => Timeline<B>, g: (b: B) => Timeline<C>) => {
    return (a: A): Timeline<C> => f(a).bind(g);
};

// --- Kleisli Arrows for Verification ---
const f_monad = (x: number): Timeline<string> => ID(`value:${x}`);
const g_monad = (s: string): Timeline<boolean> => ID(s.length > 10);
const h_monad = (b: boolean): Timeline<string> => ID(b ? "Long" : "Short");

// --- 1. Verifying Associativity ---
const fg = kleisliCompose(f_monad, g_monad);
const gh = kleisliCompose(g_monad, h_monad);

const result_LHS_monad = kleisliCompose(fg, h_monad)(12345);
const result_RHS_monad = kleisliCompose(f_monad, gh)(12345);
// LHS: 12345 -> "value:12345" -> true -> "Long"
// RHS: 12345 -> "value:12345" -> true -> "Long"
// The final Timeline value is "Long" for both, and their behaviors are equivalent

// --- 2. Verifying Left Identity ---
const id_f = kleisliCompose(ID, f_monad);
// The result of id_f(10) and f_monad(10) are both Timelines with the value "value:10", and their behaviors are equivalent

// --- 3. Verifying Right Identity ---
const f_id = kleisliCompose(f_monad, ID);
// The result of f_id(10) and f_monad(10) are both Timelines with the value "value:10", and their behaviors are equivalent

Conclusion: The Inevitability Born from the Dependency Graph

We can conclude that these mathematical laws are not abstruse constraints, but rather inevitable properties that arise from the Timeline’s dependency graph model.

• Inevitability of Functor Laws: .map() defines a static dependency. Since it defines an immutable transformation rule A -> B, it is natural that its composition follows mathematical laws.

• Inevitability of Monad Laws: On the other hand, .bind() defines a dynamic dependency. The structure of the dependency graph itself changes over time. For this complex operation of “dynamic rewiring” not to descend into unpredictable chaos, a mathematical guarantee that the result is not affected by the order of operations (associativity) is essential. The Monad laws are the inevitable rules that ensure this dynamic evolution of the graph is always orderly and predictable.

Canvas Demo (Placeholder)

(An interactive demo visually demonstrating the behavior of the Monad laws (especially associativity) will be placed here.)