Do be do be do

我们探讨了 Frank 的设计与实现，这是一种严格的函数式编程语言，具有双向效应类型系统，该系统从底层围绕 Plotkin 和 Pretnar 的效应处理器抽象的一种新颖变体构建而成。效应处理器为模块化效应编程提供了抽象：处理器充当一组命令的解释器，这些命令的接口由类型系统静态跟踪。然而，Frank 通过泛化函数抽象本身的基本机制，消除了对额外效应处理构造的需求。函数仅仅是 Frank 算子中不解释任何命令的特例。此外，Frank 的算子可以是多处理器，它们能够同时解释来自多个源的命令，而不会干扰带有值的函数式编程的直接风格。Frank 中的效应类型化采用了一种新颖的效应多态形式，避免了在源代码中提及效应变量。这是通过向内传播环境能力来实现的，而不是向外累积潜在效应的并集。我们通过示例介绍 Frank，然后对 Frank 类型系统及其语义给出形式化描述。我们通过将 Frank 算子细化为函数、case 表达式和一元处理器来引入 Core Frank，然后给出 Core Frank 的可靠小步操作语义。使用效应与处理器进行编程仍处于起步阶段。我们对未来的可能性进行了探索，特别是与其他丰富类型系统形式相结合的探索。