Idris 可以内联用作参数的函数吗？

Question

在 C++ 中，如果您要编写自己的通用 sort 函数模板，该模板接受比较谓词参数，那么编译器将能够内联该谓词。

C 中不是这种情况：qsort 被编译一次，并且它的比较谓词参数永远不会内联（也许编译器/链接器的最新技术水平最近有所改进，所以如果我的信息不正确，请纠正我-过时的）

这对 C++ 中的泛型编程来说是一个福音（当然不仅仅是sort 函数）：您可以获得相同的性能，而在 C 中，您必须放弃泛型（或使用宏）。

我的问题是：Idris 可以做 C++ 做的事情吗？它可以内联用作参数的函数吗？

Answer 1

Idris 确实支持通过注释机制对高阶函数进行部分评估。通过标记您希望在编译时传递的参数[static]，您可以获得专门化的结果程序。

参照。 the manual 了解更多详情。