Koka：使用行多态效应类型编程

我们提出了一种编程模型，其中以规范的方式处理效应，且函数的潜在副作用在其类型签名中显而易见。表达式的类型和效应也可以自动推断，我们描述了一种基于 Hindley-Milner 风格推断的多态类型推断系统。一个新颖的特性是我们通过使用重复标签的行多态性来支持多态效应。此外，我们表明我们的效应不仅仅是语法标签，而是与程序有深刻的语义联系。例如，如果一个表达式可以在没有 exn 效应的情况下被类型化，那么它永远不会抛出未处理的异常。类似于 Haskell 的 `runST`，我们展示了如何安全地封装有状态操作。通过状态效应，我们还可以安全地将状态与 let-多态性结合，而无需命令式类型变量或语法值限制。最后，我们的系统完全在一个名为 Koka 的新语言中实现，并已成功应用于各种从小到中等规模的示例程序，范围从 Markdown 处理器到分层聊天应用程序。您可以在 www.rise4fun.com/koka/tutorial 在线试用 Koka。