Zig 语言中文社区

在 zig 中实现类型安全的有限状态机

2024-11-05

sdzx

TOC

typed fsm

1. 简单介绍类型化有限状态机的优势

1.1 介绍有限状态机

有限状态机（FSM，以下简称状态机）是程序中很常见的设计模式。

它包含两个主要的概念状态和消息。状态机程序整体上的行为就是不断地产生消息，处理消息。

而状态主要是在代码层面帮助人们理解消息的产生和处理。

[1.2 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 这个例子的过程，感兴趣的可以在这里看到代码。

2.1 介绍 ATM 状态机

ATM 代表自动取款机，因此它的代码的逻辑就是模拟自动取款机的一些行为：插入银行卡，输入 pin，检查 pin，取钱，修改 pin。

它的状态机整体如下：

ATM

图中椭圆形表示状态，箭头表示消息。 它包含五种状态：exit, ready, cardInserted, session, changePin。

同时它也包含一堆的消息，每个消息都包含了系统状态的转化。 比如消息 InsertCard 代表将 ATM 的状态从 ready 转化到 cardInserted，这代表用户插入卡。

消息 Incorrect 代表将 ATM 的状态从 cardInserted 转化到 cardInserted， 这代表了一种循环，表示用户输错了 pin，但是可以再次尝试输入 pin，当然我们要求最多可以尝试三次。

整个程序效果如下：

ATM

这里注意消息 Update，它代表更新 pin，同时将状态转从 changePin 换到 ready。

ATM

实际的表现就是在 changePin 的界面中我们修改 pin，然后点击 Change 按钮触发 Update 消息，修改 pin，并返回到 ready 界面。

ATM

接下来的文章中我将修改 Update 的行为，并展示在这个过程中类型系统如何帮助我快速调整代码。

2.2 修改 Update 消息

实际的消息 Update 定义代码如下

    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

这时如果我重新编译代码，那么类型系统就会产生下面的错误：


➜  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。

修改之后的代码如下：

@call(.always_tail, cardInsertedHandler, .{ val.wit, ist });

在这里类型系统精确的告诉了我们需要修改的地方，以及原因。修改完成后程序即能正确运行。

2.3 移除 changePin 状态

这一节中我们尝试移除 changePin 状态，看看类型系统会给我们什么反馈。 如果移除 changePin，新的状态图如下：

ATM

重新编译项目，将获得类型系统的反馈

类型系统的反馈首先是：

examples/atm-gui.zig:148:36: error: enum 'atm-gui.AtmSt' has no member named 'changePin'
            ChangePin: WitFn(end, .changePin),
                                  ~^~~~~~~~~

因为 changePin 状态已经被移除，因此消息 ChangePin（它代表了从 session 进入 changePin 状态）也不应该再存在了，我们移除它再重新编译。

新的反馈如下：

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 消息，因此也将它从消息产生的地方移除，继续重新编译。

新的反馈如下：

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，由使用 haskell 实现，它实现了完整类型安全的有限状态机。

typed-fsm 基于Mcbride Indexed Monad：

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 的核心想法。看不懂不需要担心，接下来我将详细解释这些代码。

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,文章 2。

感兴趣的可以看一下，看懂这些要求你了解 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 函数。

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。

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),
        };
    }
};

接下来是消息的定义和产生，

// 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 让类型系统帮我们检查函数的调用是否正确。

通过对消息进行模式匹配，编译器能确定我们是否正确且完整的处理了所有的消息。

这些对于代码的编写，修改，重构都有巨大的帮助。

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


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() {
                ...
            }
        };
    }
};

  1. 除了 exit 状态外，其它消息需要包含 genMsg 函数用于产生消息，任何消息都必须带有 Witness

  2. 状态机都需要定义退出状态，尽管你可能永远也不会退出状态机，但退出状态作用于类型上，是不可缺少的

  3. 在互相调用其它 handler 的时候使用尾递归的语法，并且在必须在语句块最后处理消息附带的 Witness

由于 zig 的实现缺少 Mcbride Indexed Monad 语义的支持，因此类型系统不能阻止你进行下面的操作：


// 使用上面 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 例子中他们的调用方式是：

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）。出于这个语法的需要，处理函数中的 Witness 被变成了编译时已知（这里是 comptime w: AtmSt.EWitness(.ready)）。

遵循这四点要求，就能获得强大的类型安全保证，足以让你愉快的使用状态机！

5. 接下来能够增强的功能

暂时我能想到的有如下几点：

  1. 在状态机中，消息的产生和处理分开，因此可以定义多个消息产生的前端，处理部分可以任意切换消息产生的前端。比如我们可以定义测试状态机前端，用于产生测试数据，当处理部分调用测试前端的代码时就能测试整个状态机的行为。
  2. 支持子状态，这会让类型更加复杂。
  3. 开发基于typed-fsm-zig 的 gui 系统，状态机在 gui 有很高的实用性，将他们结合是一个不错的选择。
  4. 开发 typed-session-zig，实现类型安全的通信协议。我在 haskell 已经实现了一个实用的类型安全的多角色通讯协议框架，应该可以移植到 zig 中。
zoop 实现原理分析
Zig comptime 棒极了