外部函数接口
备注
Idris 的文档已在知识共享 CC0 许可下发布。因此，在法律允许的范围内，Idris 社区 已经放弃了 Idris 文档的所有版权和相关或邻近的权利。
关于CC0的更多信息，可以在网上找到：http://creativecommons.org/publicdomain/zero/1.0/
Idris 2 旨在支持多个代码生成器。默认目标是 Chez Scheme，还支持 Racket 和 Gambit 代码生成器。但是，与 Idris 1 一样，其目的是支持多个平台上的多个目标，包括例如 JavaScript、JVM、.NET 和其他尚未发明的。这使得调用其他语言函数的外部函数接口 (FFI) 的设计有点挑战，因为理想情况下它将支持所有可能的目标！
为此，Idris 2 FFI 的目标是灵活和适应性强，同时仍然支持最常见的需求，而不需要太多外部语言中的 “胶水” 代码。