Skip to content

Latest commit

 

History

History
512 lines (389 loc) · 18.4 KB

介绍类型化有限状态机.md

File metadata and controls

512 lines (389 loc) · 18.4 KB

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

1.1 介绍有限状态机

有限状态机(FSM,以下简称状态机)是程序中很常见的设计模式。

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

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

1.2 介绍typed-fsm-zig的优势

利用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, b: T, a: T) type {
    return struct {
        pub fn getMsg(self: @This()) @TypeOf(a.STM(b).getMsg) {
            if (b == a) @compileError("Can't getMsg!");
            _ = self;
            return a.STM(b).getMsg;
        }

        pub fn terminal(_: @This()) void {
            if (b != a) @compileError("Can't terminal!");
            return {};
        }
    };
}
const Exmaple = enum {
    exit,
    s1,
    s2,

    // State to Message union
    pub fn STM(s: Exmaple, b: Exmaple) type {
        return switch (s) {
            .exit => exitMsg(b),
            .s1 => s1Msg(b),
            .s2 => s2Msg(b),
        };
    }
};

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 三个参数T表示状态机的类型,b 表示终止时的状态,a,表示当前的状态。 它有两个函数,getMsg 表示从外部获取消息的函数,terminal 表示终止状态机的函数。

当b==a时表示当前处于终止状态,因此Witness只能使用terminal函数,当b!=a时表示当前不处于终止状态,应该继续从外部获取消息,因此Witness只能使用getMsg函数。

pub fn Witness(T: type, b: T, a: T) type {
    return struct {
        pub fn getMsg(self: @This()) @TypeOf(a.STM(b).getMsg) {
            if (b == a) @compileError("Can't getMsg!");
            _ = self;
            return a.STM(b).getMsg;
        }

        pub fn terminal(_: @This()) void {
            if (b != a) @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(s: Exmaple, b: Exmaple) type {
        return switch (s) {
            .exit => exitMsg(b),
            .s1 => s1Msg(b),
            .s2 => s2Msg(b),
        };
    }
};

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

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

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

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

4. 在互相调用其它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 中尾递归语法。出于这个语法的需要,处理函数中的Witness 被变成了编译时已知(这里是 comptime w: AtmSt.EWitness(.ready))。

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

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

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

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