Idrisは引数として使用される関数をインライン化できますか？

Question

C++では、比較述語引数を取る汎用のsort関数テンプレートを作成する場合、コンパイラはこの述語をインライン化することができます。

これはC言語では当てはまりません。qsortは一度コンパイルされ、その比較述語の引数は決してインライン化されません（おそらく、コンパイラ/リンカの最新の状態が改善されている可能性があります。 -date）

これは、C++の汎用プログラミングの恩恵です（もちろん、sortの機能だけではありません）.Cでは、汎用性を放棄しなければならない（またはマクロを使用する） 。

私の質問です：IdrisはC++で何をしますか？引数として使用される関数をインライン化できますか？

Answer 1

Idrisは、アノテーションメカニズムによる高次関数の部分的な評価をサポートしています。コンパイル時に渡すと予想される引数をマークすることにより、結果のプログラムを特殊化することができます。

Cf.詳細についてはthe manualをご覧ください。