diff --git a/content/post/2024-11-26-typed-fsm.md b/content/post/2024-11-26-typed-fsm.md new file mode 100644 index 0000000..a158554 --- /dev/null +++ b/content/post/2024-11-26-typed-fsm.md @@ -0,0 +1,521 @@ +--- +title: "在 zig 中实现类型安全的有限状态机" +author: sdzx +date: 2024-11-26T13:32:00+08:00 +--- +# 1. 简单介绍类型化有限状态机的优势 +## 1.1 介绍有限状态机 +有限状态机(FSM,以下简称状态机)是程序中很常见的设计模式。 + +它包含两个主要的概念状态和消息。状态机程序整体上的行为就是不断地产生消息,处理消息。 + +而状态主要是在代码层面帮助人们理解消息的产生和处理。 + +## 1.2 [typed-fsm-zig](https://github.com/sdzx-1/typed-fsm-zig) + +typed-fsm-zig 是一个利用 zig 类型系统加一些编程规范实现的一个库,用于实现类型安全的有限状态机。 + +它具有以下两点优势: +1. 类型安全,极大方便代码的编写,修改和重构 +手写状态机在实际代码中有很大的心智负担,对于它的修改和重构更是如噩梦一样。 + + typed-fsm-zig 在类型上跟踪状态机的变化,使消息的定义,产生,处理都和状态相关联,从而让类型系统帮我们检查这个过程中是否存在状态错误。 + + 在编写,修改和重构的时候,任何状态的错误都会产生编译错误,而这些编译错误能帮助我们快速找到问题,解决问题。 + + > PS:推荐在 zls 中打开保存时检查,这样你几乎能得到一个交互式的状态机开发环境。 + +2. 简单高效,无任何代码生成,能方便与现有逻辑整合 + + typed-fsm-zig 是一种编程的思想,掌握这种思想就能方便的使用它。 + + 在实际的使用中没有任何的代码生成,除了一处隐式的约束要求之外,没有任何其它的控制,开发者完全掌握状态机,因此你可以方便的将它和你现有的代码结合起来。 + +# 2. 例子:修改 ATM 状态机的状态 +这里我将以一个 ATM 状态机(以下简称 ATM)的例子来展示 typed-fsm-zig 和 zig 的类型系统如何帮助我快速修改 ATM 的状态。 + +为了简单性,这里我不展示构建 ATM 这个例子的过程,感兴趣的可以在这里看到[代码](https://github.com/sdzx-1/typed-fsm-zig/blob/master/examples/atm-gui.zig)。 + +## 2.1 介绍 ATM 状态机 +ATM 代表自动取款机,因此它的代码的逻辑就是模拟自动取款机的一些行为:插入银行卡,输入 pin,检查 pin,取钱,修改 pin。 + +它的状态机整体如下: + +![ATM](/images/typed-fsm/2.1-1.png) + +图中椭圆形表示状态,箭头表示消息。 +它包含五种状态:exit, ready, cardInserted, session, changePin。 + +同时它也包含一堆的消息,每个消息都包含了系统状态的转化。 +比如消息 InsertCard 代表将 ATM 的状态从 ready 转化到 cardInserted,这代表用户插入卡。 + +消息 Incorrect 代表将 ATM 的状态从 cardInserted 转化到 cardInserted, +这代表了一种循环,表示用户输错了 pin,但是可以再次尝试输入 pin,当然我们要求最多可以尝试三次。 + +整个程序效果如下: + +![ATM](/images/typed-fsm/2.1-2.png) + +这里注意消息 Update,它代表更新 pin,同时将状态转从 changePin 换到 ready。 + +![ATM](/images/typed-fsm/2.1-4.png) + +实际的表现就是在 changePin 的界面中我们修改 pin,然后点击 Change 按钮触发 Update 消息,修改 pin,并返回到 ready 界面。 + +![ATM](/images/typed-fsm/2.1-3.png) + +接下来的文章中我将修改 Update 的行为,并展示在这个过程中类型系统如何帮助我快速调整代码。 + +## 2.2 修改 Update 消息 +实际的消息 Update 定义代码如下 +```c + pub fn changePinMsg(end: AtmSt) type { + return union(enum) { + Update: struct { v: [4]u8, wit: WitFn(end, .ready) = .{} }, + ... + } + } + +``` +这里的.ready 就代表了处理完 Update 消息后就会进入 ready 状态。 + +我们修改这里,把它变成.cardInserted,这代表了我们要求更新完 pin 之后进入 cardInserted 界面重新输入新的 pin,这看着是个合理的要求。 + +新的状态图如下: + +![ATM](/images/typed-fsm/2.2-1.png) + + +这时如果我重新编译代码,那么类型系统就会产生下面的错误: +```shell + +➜ typed-fsm-zig git:(doc) ✗ zig build atm-gui +atm-gui +└─ run atm-gui + └─ zig build-exe atm-gui Debug native 1 errors +examples/atm-gui.zig:301:60: error: expected type 'typed-fsm.Witness(atm-gui.AtmSt,.exit,.ready)', found 'typed-fsm.Witness(atm-gui.AtmSt,.exit,.cardInserted)' + @call(.always_tail, readyHandler, .{ val.wit, ist }); + ~~~^~~~ +src/typed-fsm.zig:9:20: note: struct declared here (2 times) + return struct { + ^~~~~~ +examples/atm-gui.zig:254:46: note: parameter type declared here +pub fn readyHandler(comptime w: AtmSt.EWitness(.ready), ist: *InternalState) void { + ~~~~~~~~~~~~~~^~~~~~~~ +referenced by: + cardInsertedHander__anon_6916: examples/atm-gui.zig:271:13 + readyHander__anon_3925: examples/atm-gui.zig:261:13 + 5 reference(s) hidden; use '-freference-trace=7' to see all references + +``` +它告诉我们在 301 行存在类型不匹配。因为之前的状态是 ready 所以使用 readyHandler。 + +当我们把 Update 的状态修改为 cardInserted 时,它与 readyHandler 类型不匹配,应该将它修改为 cardInsertedHandler。 + +修改之后的代码如下: +```c + @call(.always_tail, cardInsertedHandler, .{ val.wit, ist }); +``` + +在这里类型系统精确的告诉了我们需要修改的地方,以及原因。修改完成后程序即能正确运行。 + + +## 2.3 移除 changePin 状态 + +这一节中我们尝试移除 changePin 状态,看看类型系统会给我们什么反馈。 +如果移除 changePin,新的状态图如下: + +![ATM](/images/typed-fsm/2.3-1.png) + +重新编译项目,将获得类型系统的反馈 + +类型系统的反馈首先是: +```shell +examples/atm-gui.zig:148:36: error: enum 'atm-gui.AtmSt' has no member named 'changePin' + ChangePin: WitFn(end, .changePin), + ~^~~~~~~~~ +``` +因为 changePin 状态已经被移除,因此消息 ChangePin(它代表了从 session 进入 changePin 状态)也不应该再存在了,我们移除它再重新编译。 + +新的反馈如下: + +```shell +examples/atm-gui.zig:161:64: error: union 'atm-gui.AtmSt.sessionMsg(.exit)' has no member named 'ChangePin' + if (resource.changePin.toButton()) return .ChangePin; + ~^~~~~~~~~ +``` +我们移除 ChangePin 消息,因此也将它从消息产生的地方移除,继续重新编译。 + +新的反馈如下: +```shell +examples/atm-gui.zig:296:10: error: no field named 'ChangePin' in enum '@typeInfo(atm-gui.AtmSt.sessionMsg(.exit)).@"union".tag_type.?' + .ChangePin => |wit| { + ~^~~~~~~~~ +``` +因为消息 ChangePin 已经不在了,也应将它从消息处理的地方移除,继续重新编译。 + +这一次不再有编译错误产生,我们搞定了一个新的程序,它不再包含 changePin 的逻辑。 + +在这个过程中类型系统帮助我们找到问题和原因。这非常酷!!! + + +## 2.4 总结 +以上是一个简单的例子,展示了 typed-fsm-zig 对于提升状态机编程体验的巨大效果。 + +展示类型系统如何帮助我们指示错误的地方,把复杂的状态机修改变成一种愉快的编程经历。 + +还有些没有讲到的优势如下: +1. 状态的分离,后端 handler 处理业务的状态变化,前端渲染和消息生成不改变状态。 +2. 消息生成受到类型的限制和状态相关,这样避免错误消息的产生。 + +这些优势对于复杂业务有很大的帮助。 + +接下来我将介绍 typed-fsm-zig 的原理和实现。 + +------------------------------------- +# 3. 原理与实现 +最开始的版本是[typed-fsm](https://github.com/sdzx-1/typed-fsm),由使用 haskell 实现,它实现了完整类型安全的有限状态机。 + +typed-fsm 基于[Mcbride Indexed Monad](https://hackage.haskell.org/package/typed-fsm-0.3.0.1/docs/Data-IFunctor.html): +```haskell +type a ~> b = forall i. a i -> b i + +class IMonad m where + ireturn :: a ~> m a + ibind :: (a ~> m b) -> (m a ~> m b) +``` +这是一种特殊的 monad,能在类型上为不确定状态建模。 + +而在 zig 实现中移除了对 Monad 语义的需求,保留了在类型上追踪状态的能力。 + +所以它不具备完整的类型安全的能力,需要依靠编程规范来约束代码的行为。我认为这样的取舍是值得的,它的类型安全性在 zig 中完全够用。 + +以下是一个原型例子,它包含了 typed-fsm-zig 的核心想法。看不懂不需要担心,接下来我将详细解释这些代码。 +```zig +const std = @import("std"); + +pub fn main() !void { + var val: i32 = 0; + const s1Wit = Witness(Exmaple, .exit, .s1){}; + _ = s1Handler(s1Wit, &val); +} + +pub fn Witness(T: type, end: T, start: T) type { + return struct { + pub fn getMsg(self: @This()) @TypeOf(start.STM(end).getMsg) { + _ = self; + if (end == start) @compileError("Can't getMsg!"); + return start.STM(end).getMsg; + } + + pub fn terminal(_: @This()) void { + if (end != start) @compileError("Can't terminal!"); + return {}; + } + }; +} +const Exmaple = enum { + exit, + s1, + s2, + + // State to Message union + pub fn STM(start: Exmaple, end: Exmaple) type { + return switch (start) { + .exit => exitMsg(end), + .s1 => s1Msg(end), + .s2 => s2Msg(end), + }; + } +}; + +pub fn exitMsg(_: Exmaple) void { + return {}; +} + +pub fn s1Msg(end: Exmaple) type { + return union(enum) { + Exit: Witness(Exmaple, end, .exit), + S1ToS2: Witness(Exmaple, end, .s2), + pub fn getMsg(ref: *const i32) @This() { + if (ref.* > 20) return .Exit; + return .S1ToS2; + } + }; +} +pub fn s2Msg(end: Exmaple) type { + return union(enum) { + S2ToS1: Witness(Exmaple, end, .s1), + pub fn getMsg() @This() { + return .S2ToS1; + } + }; +} + +fn s1Handler(val: Witness(Exmaple, .exit, .s1), ref: *i32) void { + std.debug.print("val: {d}\n", .{ref.*}); + switch (val.getMsg()(ref)) { + .Exit => |wit| wit.terminal(), + .S1ToS2 => |wit| { + ref.* += 1; + s2Handler(wit, ref); + }, + } +} +fn s2Handler(val: Witness(Exmaple, .exit, .s2), ref: *i32) void { + switch (val.getMsg()()) { + .S2ToS1 => |wit| { + ref.* += 2; + s1Handler(wit, ref); + }, + } +} + +``` + +首先是 Witness,它是一个类型上的证据,用来跟踪类型上状态的变化。 + +这里有一些介绍 Witness 思想的[文章 1](https://wiki.haskell.org/Type_witness),[文章 2](https://serokell.io/blog/haskell-type-level-witness)。 + +感兴趣的可以看一下,看懂这些要求你了解 GADT,上面提到的 Mcbirde Indexed Monad 本质就是在 GADT 类型上的 monad。 + +在这里的 Winess 三个参数分别表示: +1. T 表示状态机的类型, +2. end 表示终止时的状态, +3. start 表示当前的状态。 + +它还有两个函数: +1. getMsg 表示从外部获取消息的函数 +2. terminal 表示终止状态机的函数。 + +当 end == start 时表示当前处于终止状态,因此 Witness 只能使用 terminal 函数,当 end != start 时表示当前不处于终止状态,应该继续从外部获取消息,因此 Witness 只能使用 getMsg 函数。 +```c +pub fn Witness(T: type, end: T, start: T) type { + return struct { + pub fn getMsg(self: @This()) @TypeOf(start.STM(end).getMsg) { + if (end == start) @compileError("Can't getMsg!"); + _ = self; + return start.STM(end).getMsg; + } + + pub fn terminal(_: @This()) void { + if (end != start) @compileError("Can't terminal!"); + return {}; + } + }; +} + +``` + + +我们在这里定义状态。Example 包含三个状态:exit,s1,s2。我们将在类型上跟踪这些状态的变化。 + +注意这里的 STM 函数,它代表如何将状态映射到对应的消息集合。在实际 typed-fsm-zig 的代码中,这就是我所说的那一处隐式的约束要求。 + +实际代码中会将消息集合整合在 enum 的内部,使用特殊的命名规范将状态与消息集合对应。目前的隐式规范是在状态后面加上 Msg。 +```c +const Exmaple = enum { + exit, + s1, + s2, + + // State to Message union + pub fn STM(start: Exmaple, end: Exmaple) type { + return switch (start) { + .exit => exitMsg(end), + .s1 => s1Msg(end), + .s2 => s2Msg(end), + }; + } +}; + +``` + +------------------------------- +接下来是消息的定义和产生, + +```c +// exit 状态下没有任何消息 +pub fn exitMsg(_: Exmaple) void { + return {}; +} + +// s1 状态下有两个消息 Exit 和 S1ToS2, 他们分别将状态转化为 exit 和 s2 +pub fn s1Msg(end: Exmaple) type { + return union(enum) { + Exit: Witness(Exmaple, end, .exit), + S1ToS2: Witness(Exmaple, end, .s2), + + // getMsg 函数表明在 s1 状态下如何产生消息,这里受到类型系统的约束, + // 在 s1 的状态下不会产生其它状态的消息 + pub fn getMsg(ref: *const i32) @This() { + if (ref.* > 20) return .Exit; + return .S1ToS2; + } + }; +} + +// s2 状态下有一个消息 S2ToS1 +pub fn s2Msg(end: Exmaple) type { + return union(enum) { + S2ToS1: Witness(Exmaple, end, .s1), + + pub fn getMsg() @This() { + return .S2ToS1; + } + }; +} + +``` +----------------------------- +最后一部分是消息的处理。 + +整体的逻辑是通过 Witness 的 getMsg 函数从外部获取消息,然后通过模式匹配处理消息。 +每个消息又包含接下来状态的 Witness,然后使用对应的函数处理这些 Witness。 + +通过 Witness 让类型系统帮我们检查函数的调用是否正确。 + +通过对消息进行模式匹配,编译器能确定我们是否正确且完整的处理了所有的消息。 + +这些对于代码的编写,修改,重构都有巨大的帮助。 +```c +fn s1Handler(val: Witness(Exmaple, .exit, .s1), ref: *i32) void { + std.debug.print("val: {d}\n", .{ref.*}); + switch (val.getMsg()(ref)) { + .Exit => |wit| wit.terminal(), + .S1Tos2 => |wit| { + ref.* += 1; + s2Handler(wit, ref); + }, + } +} +fn s2Handler(val: Witness(Exmaple, .exit, .s2), ref: *i32) void { + switch (val.getMsg()()) { + .S2Tos1 => |wit| { + ref.* += 2; + s1Handler(wit, ref); + }, + } +} + +``` + +以上就是 typed-fsm-zig 核心想法的完整介绍。接下来我将介绍需要的编程规范。 + + +# 4. typed-fsm-zig 需要哪些编程规范 +## 1. 状态和消息集合之间需要满足的隐式命名规范 +以 ATM 为例: + +exit -- exitMsg + +ready -- readyMsg + +cardInserted -- cardInsertedMsg + +session -- sessionMsg + + +```c + +const AtmSt = enum { + exit, + ready, + cardInserted, + session, + + pub fn exitMsg(_: AtmSt) type { + return void; + } + + pub fn readyMsg(end: AtmSt) type { + return union(enum) { + ExitAtm: WitFn(end, .exit), + InsertCard: WitFn(end, .cardInserted), + + pub fn genMsg() @This() { + ... + } + }; + } + + pub fn cardInsertedMsg(end: AtmSt) type { + return union(enum) { + Correct: WitFn(end, .session), + Incorrect: WitFn(end, .cardInserted), + EjectCard: WitFn(end, .ready), + + pub fn genMsg(ist: *const InternalState) @This() { + ... + } + }; + } + + pub fn sessionMsg(end: AtmSt) type { + return union(enum) { + Disponse: struct { v: usize, wit: WitFn(end, .session) = .{} }, + EjectCard: WitFn(end, .ready), + + pub fn genMsg(ist: *const InternalState) @This() { + ... + } + }; + } +}; +``` + +## 2. 除了 exit 状态外,其它消息需要包含 genMsg 函数用于产生消息,任何消息都必须带有 Witness +## 3. 状态机都需要定义退出状态,尽管你可能永远也不会退出状态机,但退出状态作用于类型上,是不可缺少的 +## 4. 在互相调用其它 handler 的时候使用尾递归的语法,并且在必须在语句块最后处理消息附带的 Witness + +由于 zig 的实现缺少 Mcbride Indexed Monad 语义的支持,因此类型系统不能阻止你进行下面的操作: + +```c + +// 使用上面 Example 的处理函数 s1Handler, 将它修改成下面的样子。 +// 这里的 s1Handler 不应该被多次调用,在 haskell 版本的 typed-fsm 中,类型系统能检查出这里类型错误,但是在 zig 实现中无法做到, +// 因此我们要求只能在语句块最后有一个处理 Witness 的语句 +fn s2Handler(val: Witness(Exmaple, .exit, .s2), ref: *i32) void { + switch (val.getMsg()()) { + .S2Tos1 => |wit| { + ref.* += 2; + s1Handler(wit, ref); + s1Handler(wit, ref); + s1Handler(wit, ref); + s1Handler(wit, ref); + }, + } +} + +``` + +由于状态机需要长期运行,在互调递归的函数中如果不使用尾递归会导致栈溢出。 + +因此上面的 Example demo 中,如果我将 20 改成很大的值,比如二百万,那么一定会发生栈溢出,因为 demo 中的调用没采用尾递归的方式。 + +在实际的 ATM 例子中他们的调用方式是: +```c +pub fn readyHandler(comptime w: AtmSt.EWitness(.ready), ist: *InternalState) void { + switch (w.getMsg()()) { + .ExitAtm => |witness| { + witness.terminal(); + }, + .InsertCard => |witness| { + ist.times = 0; + @call(.always_tail, cardInsertedHandler, .{ witness, ist }); + }, + } +} + +``` + +这里的 `@call(.always_tail, cardInsertedHandler, .{ witness, ist })` 就是 zig 中尾递归语法(参见:[ziglang #694](https://github.com/ziglang/zig/issues/694#issuecomment-563310662))。出于这个语法的需要,处理函数中的 Witness 被变成了编译时已知(这里是 `comptime w: AtmSt.EWitness(.ready)`)。 + +遵循这四点要求,就能获得强大的类型安全保证,足以让你愉快的使用状态机! + +# 5. 接下来能够增强的功能 +暂时我能想到的有如下几点: +1. 在状态机中,消息的产生和处理分开,因此可以定义多个消息产生的前端,处理部分可以任意切换消息产生的前端。比如我们可以定义测试状态机前端,用于产生测试数据,当处理部分调用测试前端的代码时就能测试整个状态机的行为。 +2. 支持子状态,这会让类型更加复杂。 +3. 开发基于[typed-fsm-zig 的 gui 系统](https://discourse.haskell.org/t/try-to-combine-typed-fsm-with-gui-to-produce-unexpected-abstract-combinations/10026),状态机在 gui 有很高的实用性,将他们结合是一个不错的选择。 +4. 开发 typed-session-zig,实现类型安全的通信协议。我在 haskell 已经实现了一个[实用的类型安全的多角色通讯协议框架](https://github.com/sdzx-1/typed-session),应该可以移植到 zig 中。 diff --git a/static/images/typed-fsm/2.1-1.png b/static/images/typed-fsm/2.1-1.png new file mode 100644 index 0000000..978044c Binary files /dev/null and b/static/images/typed-fsm/2.1-1.png differ diff --git a/static/images/typed-fsm/2.1-2.png b/static/images/typed-fsm/2.1-2.png new file mode 100644 index 0000000..bb5c5df Binary files /dev/null and b/static/images/typed-fsm/2.1-2.png differ diff --git a/static/images/typed-fsm/2.1-3.png b/static/images/typed-fsm/2.1-3.png new file mode 100644 index 0000000..d09e20b Binary files /dev/null and b/static/images/typed-fsm/2.1-3.png differ diff --git a/static/images/typed-fsm/2.1-4.png b/static/images/typed-fsm/2.1-4.png new file mode 100644 index 0000000..4d6e5c3 Binary files /dev/null and b/static/images/typed-fsm/2.1-4.png differ diff --git a/static/images/typed-fsm/2.2-1.png b/static/images/typed-fsm/2.2-1.png new file mode 100644 index 0000000..bb28044 Binary files /dev/null and b/static/images/typed-fsm/2.2-1.png differ diff --git a/static/images/typed-fsm/2.3-1.png b/static/images/typed-fsm/2.3-1.png new file mode 100644 index 0000000..2782697 Binary files /dev/null and b/static/images/typed-fsm/2.3-1.png differ