利用函数式事件溯源消除业务逻辑 Bug

Nadeem Bitar 2026-05-04 4.7 KB 27.5K 201 𝕏 文章列表

文章介绍了一种基于函数式事件溯源（Functional Event Sourcing）的库，旨在让业务逻辑 Bug 在结构上不可能发生。作者通过定义可组合的状态机，在类型层统一描述状态转换，自动生成决策逻辑和演化逻辑，从而避免两者不一致。此外，该库还能自动生成 Mermaid 流程图，并利用 SMT 求解器验证业务不变性，大幅提升代码的健壮性和可维护性。

函数式编程事件溯源状态机领域驱动设计 SMT 形式化验证架构设计代码质量 Haskell

# Making Business-Logic Bugs Structurally Impossible **作者**: Nadeem Bitar **日期**: 2026-05-03T15:41:22.000Z **来源**: [https://x.com/shinzui/status/2050963939060838501](https://x.com/shinzui/status/2050963939060838501) --- ![Image](/doc/1541/image/img_85d57eab5f15.jpg) I've been building a library that aims to make business-logic bugs almost impossible to ship, even when the code is generated by a coding agent. The foundation is functional event sourcing which we've been using in production for a few years. In functional event sourcing your business logic lives in a small pure module: trivial to test, trivial to debug, trivial to reason about. ``` data Decider c e s = Decider { decide :: c -> s -> [e] , evolve :: s -> e -> s , initialState :: s , isTerminal :: s -> Bool } ``` …and you write it by hand: ``` userReg :: Decider UserCmd UserEvent UserState userReg = Decider { decide = \cmd s -> case (s, cmd) of (PotentialCustomer, Start d) -> [RegistrationStarted d.email d.confirmCode d.at] (RequiresConfirmation r, Confirm d) | d.code == r.confirmCode -> [AccountConfirmed r.email d.at] | otherwise -> [] (RequiresConfirmation r, Resend d) -> [ConfirmationResent r.email d.code d.at] (RequiresConfirmation r, Gdpr d) -> [AccountDeleted r.email d.at] _ -> [] , evolve = \s ev -> case (s, ev) of (PotentialCustomer, RegistrationStarted email code at) -> Registering { email, confirmCode = code, registeredAt = at } (Registering r, ConfirmationEmailSent _) -> RequiresConfirmation r (RequiresConfirmation r, AccountConfirmed _ at) -> Confirmed r { confirmedAt = at } (RequiresConfirmation r, ConfirmationResent _ code at) -> RequiresConfirmation r { confirmCode = code, registeredAt = at } (_, AccountDeleted _ at) -> Deleted at (s, _) -> s , initialState = PotentialCustomer , isTerminal = \case Deleted{} -> True; _ -> False } ``` The catch is that hand-written deciders carry their share of bugs. Missed branches. decide and evolve quietly drifting out of sync, so a freshly produced event no longer round-trips through replay and invariants are violated. So over the last few weekends I've been working on a library that aims to make those bugs structurally impossible to write. Workflows are composable state machines defined at the type level. You describe each edge once, and both decide and evolve are derived from that single definition, so they can never disagree. A small DSL hides the type-level machinery, so day-to-day code looks like the decider: ``` userReg = buildTransducer PotentialCustomer emptyRegs do from PotentialCustomer do onCmd inCtorStart \d -> do slot @"email" .= d.email slot @"confirmCode" .= d.confirmCode slot @"registeredAt" .= d.at emit wireRegistrationStarted goto Registering from RequiresConfirmation do onCmd inCtorConfirm \d -> do requireEq d.confirmCode #confirmCode slot @"confirmedAt" .= d.at emit wireAccountConfirmed goto Confirmed onCmd inCtorResend \d -> do slot @"confirmCode" .= d.code slot @"registeredAt" .= d.at emit wireConfirmationResent goto RequiresConfirmation onCmd inCtorGdpr \d -> do slot @"deletedAt" .= d.at goto Deleted ``` Notice what's missing: there is no separate evolve. Replay is generated from the same edge definition that produced the event, so the two directions can't fall out of sync. Two more things fall out for free. 1) Mermaid diagrams generated straight from the code, so you can visually verify what you actually wrote, in code review or a design doc: ![Image](/doc/1541/image/img_a1527d20550d.jpg) 2) An SMT-backed checker you can run on CI. Encode a business invariant ("no path reaches Confirmed without the code-equality guard firing," "every started registration eventually reaches a terminal state," "deletedAt is never set on a non-terminal vertex") and the solver either proves it or hands you the counter-example trace. The kind of bug a code review will not easily catch. Really happy with what I have so far. Still a fair bit of work before I'd use it at work, but the core is there. ## 相关链接 - [Nadeem Bitar](https://x.com/shinzui) - [@shinzui](https://x.com/shinzui) - [12K](https://x.com/shinzui/status/2050963939060838501/analytics) - [11:41 PM · May 3, 2026](https://x.com/shinzui/status/2050963939060838501) - [12.5K Views](https://x.com/shinzui/status/2050963939060838501/analytics) - [View quotes](https://x.com/shinzui/status/2050963939060838501/quotes) --- *导出时间: 2026/5/4 11:40:58* --- ## 中文翻译 # 从结构上杜绝业务逻辑 Bug **作者**: Nadeem Bitar **日期**: 2026-05-03T15:41:22.000Z **来源**: [https://x.com/shinzui/status/2050963939060838501](https://x.com/shinzui/status/2050963939060838501) --- ![Image](/doc/1541/image/img_85d57eab5f15.jpg) 我正在构建一个库，旨在让业务逻辑 Bug 几乎不可能被带上线，即使代码是由编程代理生成的。其基础是函数式事件溯源，我们已经在生产环境中使用它几年了。在函数式事件溯源中，你的业务逻辑位于一个微小的纯模块中：极易测试，极易调试，极易推理。 ``` data Decider c e s = Decider { decide :: c -> s -> [e] , evolve :: s -> e -> s , initialState :: s , isTerminal :: s -> Bool } ``` ……并且你需要手写它： ``` userReg :: Decider UserCmd UserEvent UserState userReg = Decider { decide = \cmd s -> case (s, cmd) of (PotentialCustomer, Start d) -> [RegistrationStarted d.email d.confirmCode d.at] (RequiresConfirmation r, Confirm d) | d.code == r.confirmCode -> [AccountConfirmed r.email d.at] | otherwise -> [] (RequiresConfirmation r, Resend d) -> [ConfirmationResent r.email d.code d.at] (RequiresConfirmation r, Gdpr d) -> [AccountDeleted r.email d.at] _ -> [] , evolve = \s ev -> case (s, ev) of (PotentialCustomer, RegistrationStarted email code at) -> Registering { email, confirmCode = code, registeredAt = at } (Registering r, ConfirmationEmailSent _) -> RequiresConfirmation r (RequiresConfirmation r, AccountConfirmed _ at) -> Confirmed r { confirmedAt = at } (RequiresConfirmation r, ConfirmationResent _ code at) -> RequiresConfirmation r { confirmCode = code, registeredAt = at } (_, AccountDeleted _ at) -> Deleted at (s, _) -> s , initialState = PotentialCustomer , isTerminal = \case Deleted{} -> True; _ -> False } ``` 问题在于，手写的决策器难免带有一些 Bug。遗漏分支。`decide` 和 `evolve` 悄悄地步调不一致，导致新生成的事件在重放时无法正确地进行往返，不变量因此被破坏。所以在过去几个周末，我一直在开发一个库，旨在从结构上让这些 Bug 根本无法被写出来。工作流是在类型层级定义的可组合状态机。你只需描述一次每条边，`decide` 和 `evolve` 都是从这唯一的定义中派生出来的，所以它们永远不可能不一致。一个小型的 DSL 隐藏了类型层级的机制，使得日常代码看起来就像决策器一样： ``` userReg = buildTransducer PotentialCustomer emptyRegs do from PotentialCustomer do onCmd inCtorStart \d -> do slot @"email" .= d.email slot @"confirmCode" .= d.confirmCode slot @"registeredAt" .= d.at emit wireRegistrationStarted goto Registering from RequiresConfirmation do onCmd inCtorConfirm \d -> do requireEq d.confirmCode #confirmCode slot @"confirmedAt" .= d.at emit wireAccountConfirmed goto Confirmed onCmd inCtorResend \d -> do slot @"confirmCode" .= d.code slot @"registeredAt" .= d.at emit wireConfirmationResent goto RequiresConfirmation onCmd inCtorGdpr \d -> do slot @"deletedAt" .= d.at goto Deleted ``` 请注意少了什么：这里没有单独的 `evolve`。重放逻辑是从产生事件的同一条边定义中生成的，所以这两个方向不可能步调不一致。此外，还免费获得了另外两个功能。 1) 直接从代码生成 Mermaid 图，这样你可以在代码审查或设计文档中直观地验证你实际写的内容： ![Image](/doc/1541/image/img_a1527d20550d.jpg) 2) 一个支持 SMT 的检查器，你可以在 CI 中运行它。编码一个业务不变量（“没有路径能在不触发 code-equality 守卫的情况下到达 Confirmed 状态”，“每个已开始的注册最终都会到达终止状态”，“deletedAt 从不会在非终止节点上被设置”），求解器要么证明它，要么给你反例轨迹。这正是代码审查很难发现的那类 Bug。我对目前的进展非常满意。虽然距离在工作中使用还有一些工作要做，但核心功能已经实现了。 ## 相关链接 - [Nadeem Bitar](https://x.com/shinzui) - [@shinzui](https://x.com/shinzui) - [12K](https://x.com/shinzui/status/2050963939060838501/analytics) - [11:41 PM · May 3, 2026](https://x.com/shinzui/status/2050963939060838501) - [12.5K Views](https://x.com/shinzui/status/2050963939060838501/analytics) - [View quotes](https://x.com/shinzui/status/2050963939060838501/quotes) --- *导出时间: 2026/5/4 11:40:58*