Koka：一种具有效果的函数式语言

Koka v3 是一种正在开发中的研究语言，尚不适合生产使用。

最新版本：v3.1.2，2024-05-30（[安装]）。

Koka 是一种具有效果类型和处理器的强类型函数式风格语言。

Koka 的核心由一小组经过充分研究的语言特性组成，如一级函数、多态类型和效果系统、代数数据类型以及效果处理器。每一项都是可组合的，通过尽可能通用来避免添加"特殊"扩展。
Koka 在其类型中跟踪每个函数的（副）效果，区分纯函数和有效果的计算。精确的效果类型赋予 Koka 坚如磐石的语义，这些语义由经过充分研究的范畴论支持，使 Koka 对人类和编译器都特别容易推理。
_效果处理器_让你能够以类型安全和可组合的方式将高级控制抽象（如异常、异步/等待或概率程序）定义为用户库。
Perceus 是一种先进的引用计数编译方法。与[证据传递][evidence]结合使用，这使 Koka 能够直接编译为 C 代码，无需垃圾收集器或运行时系统。Perceus 还执行重用分析，并在可能的情况下优化函数式风格的程序以使用就地更新。

了解更多：

[安装] Koka 并编译你的第一个程序。
阅读 [Koka 手册][kokabook]，了解 Koka 语言的概览及其规范。
浏览[库文档][libraries]。
帮助开发

享受编程， Daan Leijen

特别感谢：Tim Whiting 和 Fredrik Wieczerkowski 在 VS Code 语言集成方面的工作， Anton Lorenzen 在单孔上下文（[pdf][fiptree-tr]）、完全就地编程[11]和 Perceus 中有限帧重用[10]方面的工作，Ningning Xie 在证据传递理论和实践[9,6]以及 Perceus 引用计数形式化[8]方面的工作， Alex Reinking 在实现 Perceus 引用计数分析[8]方面的工作，以及所有在 Koka 早期版本上工作的实习生：Daniel Hillerström、Jonathan Brachthäuser、Niki Vazou、Ross Tate、Edsko de Vries 和 Dana Xu。

近期版本

v3.1.2，2024-05-30：修复不在工作区时 VS Code 安装问题。
v3.1.1，2024-03-04：修复语言服务器崩溃问题；修复在较旧 gcc 版本上的构建问题。
v3.1.0，2024-02-14：新的并发构建系统和改进的模块依赖跟踪 -- 构建速度大大提高。语言服务器现在通过 --language-server --lsstdio 标志组合支持 stdio 协议。清理证据向量 API，移除 C 后端的 cfc 支持。内部重新设计（命名）效果生成，以更紧密匹配形式系统。
v3.0.4，2024-01-25：修复隐式无限扩展的 bug。将 std/core 拆分为多个模块，改进 VS Code 中的悬停和内嵌信息，修复各种小 bug。
v3.0.1，2024-01-13：修复表达式求值中的小 bug，修复 macOS 上的区域设置错误。
v3.0.0，2024-01-13：改进 VS Code 语言支持，增加内嵌提示。新增局部限定名称，初步支持隐式参数。示例可在 samples/syntax 中找到。修复各种 bug。
v2.6.0，2023-12-30：初步支持 VS Code 语言服务，包括类型信息、跳转到定义、直接从编辑器运行测试函数、自动 Koka 安装等多项功能。特别感谢 Tim Whiting 和 Fredrik Wieczerkowski 为实现这一切所做的所有工作！还包括对单孔上下文的支持（[pdf][fiptree-tr]）和扩展的 int32/int64 位运算，以及各种 bug 修复。
v2.4.2，2023-07-03：中期发布，支持新的 fip 和 fbip 关键字，以支持完全就地编程[11]。修复各种 bug 并提高性能。
v2.4.0，2022-02-07：自动生成各种 Linux 发行版的安装包（由 Rubikscraft 完成），改进专门化和整数加/减，添加 rbtree-fbip 示例，改进语法（pub（替代 public，移除 private（因为它始终是默认的）），final ctl（替代 brk），数字字面量中的下划线等），将 double 重命名为 float64，修复各种 bug。

安装

Koka 为 Windows（x64）、macOS（x64、M1）和 Linux（x64）提供[二进制安装程序][install]。对于其他平台，你需要从源代码构建编译器。

从源代码构建

Koka 的依赖很少，应该可以在大多数常见平台上轻松从源代码构建，例如 Windows（包括 WSL）、macOS 和 Unix。构建 Koka 需要以下程序：

Stack 用于运行 Haskell 编译器。在 macOS 上使用 brew install haskell-stack，在 Unix 上使用 curl -sSL https://get.haskellstack.org/ | sh，或在 Windows 上使用二进制安装程序。
可选：[vcpkg] 用于轻松链接 C 库。在 macOS 上使用 brew install vcpkg。在其他系统上使用 vcpkg [安装][vcpkg] 说明（如果安装到 ~/vcpkg，Koka 可以自动找到 vcpkg）。
可选：如果使用 Javascript 后端，需要 nodejs。
可选：如果使用 Wasm 后端，需要 [emscripten] 和 [wasmtime]。
可选：在 Windows 上建议安装 [clang][winclang] C 编译器（使用 LLVM-<version>-win64.exe），或 Visual Studio C 编译器。
在 Windows 上，首先将控制台代码页设置为 UTF8 以避免 stack 构建错误：$ chcp 65001。

现在克隆仓库并按以下方式构建编译器：

$ git clone --recursive https://github.com/koka-lang/koka
$ cd koka
$ stack update
$ stack build
$ stack exec koka

(注意:如果克隆时忘记添加 --recursive 参数,在编译 Koka 模块时会出现错误 -- 可以通过运行 git submodule update --init --recursive 来纠正)。

您也可以使用 stack build --fast 构建编译器的调试版本, 并使用 stack test --fast 运行测试套件。

要运行单个测试,您可以根据路径进行过滤,例如 stack test --test-arguments '-m "lib"'。这将运行 test/lib 目录下的所有测试。

(如果在运行或安装 stack 时遇到问题,请参阅下面的构建说明)。

创建安装包

Koka 可以生成一个可以在本地机器上安装的二进制安装包:

$ stack exec koka -- -e util/bundle
...
distribution bundle created.
  bundle : bundle/v2.3.9/koka-v2.3.9-linux-x64.tar.gz
  cc     : gcc
  version: v2.3.9

这需要一些时间,因为它会预编译标准库的三个构建变体(debug、drelease(带调试信息的发布版)和 release)。生成安装包后,您可以在本地安装:

$ util/install.sh  bundle/v2.3.9/koka-v2.3.9-linux-x64.tar.gz

(在 Windows 上使用 util/install.bat)。安装后,您现在可以直接调用 koka:

$ koka --version

默认情况下,Koka 会为当前用户安装在 <prefix>/bin/koka, (特定架构的文件位于 <prefix>/lib/koka/v2.x.x 下, 库和示例位于 <prefix>/share/koka/v2.x.x 下)。在 Unix 和 macOS 上,默认前缀是 /usr/local, 在 Windows 上,默认前缀是 %LOCALAPPDATA%\koka。

也可以为各种 Linux 平台(RHEL、Debian、Alpine 等)生成安装包。更多信息请参阅[自述文件][util/packaging]。

基准测试

这些是使用 [Perceus] 引用计数的 Koka v2 与其他各种语言中最先进的内存回收实现的初步基准测试。由于我们在不同语言之间进行比较,我们需要谨慎解读这些结果 -- 结果不仅取决于内存回收,还取决于每个编译器执行的不同优化以及我们如何将每个基准测试转换到特定语言。因此,我们主要将这些结果视为 当前 Koka 引用计数实现可行且具有竞争力的证据,而不是语言和系统之间绝对性能的直接比较。

因此,我们在这里只选择强调内存分配的基准测试,并尝试选择使用一系列内存回收技术且被认为是同类最佳的成熟比较系统。我们比较的系统包括 Koka 2.0.3(使用 gcc 9.3.0 编译生成的 C 代码)、OCaml 4.08.1、Haskell GHC 8.6.5、Swift 5.3、使用 Hotspot G1 收集器的 Java SE 15.0.1 以及 C++ gcc 9.3.0。

所有基准测试都可在 test/bench 中找到(有关构建说明,请参阅那里的自述文件),它们都强调内存分配,计算量很小: rbtree(向红黑树中插入 4200 万个项目), rbtree-ck(rbtree 的一个变体,保留每第 5 个子树的列表,因此共享许多子树),deriv (大型表达式的符号导数), nqueens(计算大小为 13 的 n 皇后问题的所有解决方案到一个列表中,并返回该列表的长度,其中解决方案列表共享许多子解决方案),以及 cfold(对大型符号表达式进行常量折叠)。

注意:在 C++ 中,由于没有自动内存管理,许多基准测试很难直接表达,因为它们使用持久和部分共享的数据结构。要忠实地实现这些,本质上需要手动引用计数。相反,我们使用 C++ 作为性能基准:我们要么使用就地更新而不支持持久性(如在使用 std::map 的 rbtree 中),要么根本不回收内存(如在 deriv、nqueens 和 cfold 中)。

右图显示了平均 10 次运行的执行时间和峰值工作集,并归一化为 Koka(在运行 Ubuntu 20.04 的 3.8Ghz AMD3600XT 上,2020 年 11 月)。

我们可以看到,尽管 Koka 目前除了引用计数优化外几乎没有其他优化,但与这些成熟系统相比,它的表现非常好,通常在执行时间和峰值工作集方面都明显优于它们。显然,这些基准测试是分配密集型的,但看到 Koka 的初始性能令人鼓舞。

这些基准测试和系统的完整讨论可以在 [Perceus] 报告中找到。

任务

请帮助开发 Koka:有许多机会来改进 Koka 或用 Koka 进行研究。我们需要:

Emacs(部分完成)和 Vim 语法高亮。
添加更多示例,改进文档、登陆页面等。使人们更容易做出贡献。
运行完整的测试套件。
使用大参数运行贝叶斯概率机器学习程序。
参数中带有模式匹配的函数(由 Steven Fontanella 完成)。
支持 int64 操作

更高级的项目:

硕士/博士级别:

更好的语言级 FBIP 支持,具有保证的数据类型匹配、自动导数和访问者生成。
浮动 open 调用以改进效果处理(由 Naoya Furudono 负责)
形式化开放和关闭效果行类型(由 Kazuki Ikemori 负责)
我们能否使用 C++ 异常来实现"零成本" if yielding() ... 分支并消除连接点的需求(参见[9])。
使用形状信息改进已知情况的简化

目前正在进行的工作:

各种标准优化,如 case-of-case、连接点、case-of-known 构造函数等。
实现内联专门化,其中像 map、fold 等函数会针对调用它们的函数进行专门化。这是函数式语言的重要优化,可以减少 lambda 的分配。 (联系人:Steven Fontanella)
Perceus 的借用分析和改进的重用分析。(联系人:Anton Lorenzen)

以下是未来几个月要完成的直接待办事项列表:

移植带有 libuv 集成的 std/async。
通过隐式参数初步支持重载。

LSP 相关任务:

为效果处理程序生成补全(包含所有函数的空主体)
为数据类型生成 show / (==)
查找引用
生成类型注释

扩展相关任务:

VSCode:

添加对调试可执行文件的支持

如果您对解决其中一些问题感兴趣,请与我联系 :-)

构建说明

分支

主要开发分支是:

master: 最新稳定版本。
dev: 当前开发分支 -- 提交 PR 到这个分支。
v1-master: Koka v1 的最后一个稳定版本:这是带有 JavaScript(和 C#) 后端的 Koka,不使用证据转换。这个版本支持 std/async 并应该能够编译已发表论文中的示例。

在 macOS M1 上构建

你需要至少 stack 版本 >= 2.11 此外,你可能需要将 brew 安装的 LLVM 添加到你的路径中,否则 stack 找不到 LLVM 工具。将以下内容添加到你的 ~/.zshrc 脚本中并打开一个新的提示符:

export PATH=/opt/homebrew/opt/llvm/bin:$PATH

使用 Cabal 构建

某些平台（如Linux arm64和FreeBSD）并不总是很好地支持stack。在这些情况下，我们也可以直接使用ghc和cabal。按如下方式安装这些包：

$ sudo apt update
$ sudo apt install ghc cabal-install

在macOS（x64和arm64）上，我们使用brew：

$ brew install pkg-config ghc cabal-install

在FreeBSD上，使用pkg：

$ sudo pkg update
$ sudo pkg install ghc hs-cabal-install   # 或者：hs-haskell-platform

可选地，也安装vcpkg。如果你将其安装在~/vcpkg目录下，Koka会在需要时自动找到它：

~$ git clone https://github.com/microsoft/vcpkg
~$ ./vcpkg/bootstrap-vcpkg.sh
~$ vcpkg/vcpkg install pcre

现在我们可以使用cabal来构建编译器：

~$ git clone --recursive https://github.com/koka-lang/koka
~$ cd koka
~/koka$ cabal new-update
~/koka$ cabal new-build
~/koka$ cabal new-run koka

我们也可以运行测试：

~/koka$ cabal new-run koka-test

或创建安装程序：

~/koka$ cabal new-run koka -- -e util/bundle

使用minbuild构建

如果stack和cabal都无法使用，你可以尝试运行最小构建脚本来构建Koka：

~/koka$ ./util/minbuild.sh

这会直接调用ghc来构建编译器。你可以从minbuild创建一个安装包：

~/koka$ .koka/minbuild/koka -e util/bundle.kk -- --koka=.koka/minbuild/koka

Windows C编译器

Windows上的Koka编译器需要一个C编译器。默认情况下，当使用stack exec koka时，会使用ghc提供的C编译器（mingw），但它只在stack环境中可见。

因此，建议安装Windows版的[clang][winclang]编译器（运行util/install.bat时会自动安装）。不过，如果你从Visual Studio x64工具集命令提示符运行koka，Koka也可以使用Microsoft Visual C++编译器（cl）（以便正确链接Windows系统库）。

通常，对于Koka代码，mingw（gcc）的优化效果最好，紧随其后的是clang-cl。在3.8GHz AMD 3600XT上，使用mingw 7.2.0、clang-cl 11.0.0和cl 19.28，我们得到：

$ stack exec out\v2.0.5\mingw-release\test_bench_koka_rbtree -- --kktime
420000
info: elapsed: 0.624s, user: 0.625s, sys: 0.000s, rss: 163mb

$ out\v2.0.5\clang-cl-release\test_bench_koka_rbtree --kktime
420000
info: elapsed: 0.727s, user: 0.734s, sys: 0.000s, rss: 164mb

$ out\v2.0.5\cl-release\test_bench_koka_rbtree --kktime
420000
info: elapsed: 1.483s, user: 1.484s, sys: 0.000s, rss: 164mb

语言服务器

查看support/vscode/README.md了解如何构建VS Code语言服务器。

旧版本发布说明

v2.3.8，2021-12-27：改进int性能，修复各种bug，更新wasm后端，初步支持conan，修复js后端。
v2.3.6，2021-11-26：修复特化bug，添加std/os/readline模块。
v2.3.4，2021-11-26：maybe类型已经是值类型，但现在如果不嵌套，也不需要堆分配（[Just(1)]使用与[1]相同的堆空间），改进原子引用计数（由Anton Lorenzen完成），改进特化（由Steven Fontanella完成），各种小修复，修复在freeBSD上的构建。
v2.3.2，2021-10-15：初步支持wasm（使用--target=wasm，并安装[emscripten]和[wasmtime]），改进重用特化（由Anton Lorenzen完成），修复非深色shell的默认配色方案（#190），无堆栈的释放和标记，添加--stack选项，支持[musl]（使用--cc=musl-gcc），修复macOS上使用homebrew安装vcpkg的vcpkg支持，修复各种bug。
v2.3.1，2021-09-29：改进TRMC优化和重用（rbtree基准测试现在比C++更快）。改进效果操作速度。允许在匿名函数表达式（如xs.map( fn(x) x + 1 )）和操作子句中省略->。允许使用ctl代替control。新的默认输出目录为.koka，改进命令行选项以更符合其他编译器（使用-o指定最终输出，使用-e执行程序）。
v2.3.0，2021-09-20：许多变更：新的布局规则可以[省略大括号][nobrace]，不再需要给if和match条件加括号（参见samples/basic/rbtree示例），更新JavaScript后端（--target=js）以使用标准ES6模块和新的[BigInt][bigint]用于任意精度整数，改进运行时布局以支持128位arm CHERI，添加std/num/int64模块和int64原始类型，添加binarytrees基准测试，初步支持并行任务（在std/os/task中），改进简化和内联，大大改进效果操作，更新交互环境的isocline。
v2.2.1，2021-09-05：改进优化，初步支持并行任务，二叉树基准测试，效果处理仍略慢，升级isocline，修复小bug。
v2.2.0，2021-08-26：改进已知情况的简化（由Rakshika B完成），改进跨模块特化（由Steven Fontanella完成），初步借用注解和改进重用分析（由Anton Lorenzen完成），改进交互环境的行编辑，改进内联。注意：由于新的内联阶段，在此版本中效果处理可能稍慢，但将在下一版本中改进。
v2.1.9，2021-06-23：初步支持跨模块特化（由Steven Fontanella完成）。
v2.1.8，2021-06-17：初步支持macOS M1和Linux arm64，改进readline，小修复。
v2.1.6，2021-06-10：初步支持浅恢复，修复向量的空间泄漏，允许使用--fasan的gcc，改进vcpkg支持，添加--fstdalloc标志，改进VS code语法高亮，改进valgrind支持，添加--no-optimize标志以获取更多调试信息。
v2.1.4，2021-05-31：移除对cmake的依赖，支持库链接，支持vckpg，更新std/text/regex，改进Windows安装程序，包含clang安装，移除对Windows上Visual Studio的依赖，改进--fasan支持，修复装箱值类型的空间泄漏，内部使用有符号size_t，修复各种小bug。
v2.1.2，2021-05-01：修复各种bug，允许在匿名函数参数中使用模式绑定（由Steven Fontanella完成），初步支持Emacs语法高亮（由Kamoii完成）。
v2.1.1，2021-03-08：修复bug，使用右结合的(++)进行字符串和列表连接（而不是(+)），改进内部字符串处理。
v2.0.16，2021-02-14：修复bug，修复逻辑运算的短路求值，改进utf-8处理。
v2.0.14，2020-12-11：修复bug，改进变量逃逸检查。
v2.0.12，2020-12-02：支持VS Code和Atom的语法高亮，改进卸载，更多示例。
v2.0.9，2020-11-27：现在提供Windows、macOS和Linux的二进制[发布版][releases]。
v2.0.7，2020-11-23：更多小修复，改进作用域处理器，改进高阶类型传播，更多示例。
v2.0.5，2020-11-15：修复许多bug并改进。改进代码生成，命名处理器，添加示例，支持docker，直接C编译，支持本地安装。
v2.0.0，2020-08-21：初始v2发布。

参考文献

Daniel Hillerström和Sam Lindley。"用行和处理器解放效果。"发表于《第一届类型驱动开发国际研讨会论文集》，15--27页。TyDe 2016。日本奈良。2016年。doi:10.1145/2976022.2976033。
Daan Leijen。"Koka：使用行多态效果类型编程。"发表于《2014年数学结构化函数式编程》。EPTCS。2014年3月。arXiv:1406.2061。
Daan Leijen。《函数式编程的代数效应》。MSR-TR-2016-29。微软研究院。2016年8月。https://www.microsoft.com/en-us/research/publication/algebraic-effects-for-functional-programming。[4]的扩展版本。
Daan Leijen。"行类型代数效应的类型导向编译。"发表于《编程语言原理会议（POPL'17）论文集》。法国巴黎。2017年1月。
Nicolas Wu、Tom Schrijvers和Ralf Hinze。"作用域内的效应处理器。"发表于《2014年ACM SIGPLAN Haskell研讨会论文集》，第1-12页。Haskell '14。ACM，美国纽约。2014年。doi:10.1145/2633357.2633358
Ningning Xie、Jonathan Brachthäuser、Daniel Hillerström、Philipp Schuster、Daan Leijen。"效应处理器，显然" 第25届ACM SIGPLAN国际函数式编程会议（ICFP），2020年8月。doi:10.1145/3408981，pdf。另见[9]，该文对此工作进行了改进。
Ningning Xie和Daan Leijen。"Haskell中的效应处理器，显然"第13届ACM SIGPLAN国际Haskell研讨会，2020年8月。 pdf 另见Ev.Eff和Mp.Eff代码库。
Alex Reinking、Ningning Xie、Leonardo de Moura和Daan Leijen："Perceus：具有重用功能的无垃圾引用计数"MSR-TR-2020-42，2020年11月22日。PLDI'21杰出论文。 pdf
Ningning Xie和Daan Leijen。"效应处理器的广义证据传递"发表于第26届ACM SIGPLAN国际函数式编程会议（ICFP），2021年8月。同时作为MSR-TR-2021-5，2021年3月。 pdf
Anton Lorenzen和Daan Leijen。"帧限制重用的引用计数"微软研究院技术报告MSR-TR-2021-30，2021年11月（2022年3月更新，v2）。pdf
Anton Lorenzen、Daan Leijen和Wouter Swierstra。"FP²：完全原地函数式编程" 第28届ACM SIGPLAN国际函数式编程会议（ICFP），2023年9月。 pdf（扩展技术报告MSR-TR-2023-19，2023年5月）。