如何在Idris2 FFI中让纯外部函数在REPL中独立求值？

1. 让外部纯函数在REPL中直接求值的修改方案 #

要实现目标，需完成以下操作：

• 标记FFI函数为纯函数：在%foreign声明末尾添加total关键字，告知编译器该函数无副作用、可安全求值。示例代码：

  add : Int -> Int -> Int
  add = %foreign "C:add,libadd" total
  

  没有total标记时，REPL会默认认为外部函数可能存在副作用，不会主动求值，仅返回表达式本身。

• 确保共享库可被找到：

  • 将编译好的共享库（如libadd.so、libadd.dylib或add.dll）放入系统默认库路径；
  • 启动REPL时通过--libdir参数指定库所在目录，例如：idris2 --libdir ./lib your_module.idr；
  • 在模块开头添加%link "libadd"声明，显式告诉编译器链接该库。

修改完成后，在REPL中直接输入add 70 24即可得到计算结果。

2. 内置(+)可正常工作的原因 #

内置算术函数如(+)是Idris2编译器的核心实现部分，并非通过FFI调用外部C函数：

• 这些函数的逻辑直接内嵌在编译器的代码生成后端（如RefC、LLVM）中，编译时会直接生成对应机器码，无需依赖外部共享库；
• 编译器原生知晓这些函数是纯函数、无副作用且完全可计算，因此REPL会直接对其表达式求值，而非返回原表达式；
• 它们默认被标记为total，符合Idris2的纯函数求值规则，无需额外声明。

内容的提问来源于stack exchange，提问作者thor