En C++, si vous deviez écrire votre propre modèle de fonction générique sort qui prend un argument de prédicat de comparaison, le compilateur serait en mesure d'intégrer ce prédicat. Ce n'est pas le cas dans C: qsort est compilé une fois, et son argument de prédicat de comparaison n'est jamais inline (Peut-être l'état de l'art du compilateur/éditeur de liens s'est amélioré dernièrement, alors corrigez-moi si mes informations sont hors de -date)Can Idris inline fonctions qui sont utilisées comme arguments?
Ceci est un avantage pour la programmation générique en C++ (pas seulement la fonction sort, bien sûr): vous pouvez obtenir les mêmes performances, pour lesquelles en C, vous devez abandonner la généricité (ou utiliser des macros) .
Ma question est: est-ce que Idris peut faire ce que C++ fait ici? Peut-il intégrer des fonctions utilisées comme arguments?