如何将Idris作为纯Haskell库使用？求示例代码

确实，Idris的Haskell库API文档一直是个痛点，很多时候得靠翻源码（比如Idris.Main、Idris.Core这些核心模块）逆向工程才能搞明白用法。不过别担心，我结合你给出的示例代码，整理了一套可行的实现方案，包括完整的可运行代码和关键注意事项。

核心流程概述 #

Idris的Haskell库提供了一套会话式API，用来加载、检查、求值Idris代码，基本步骤是：

• 初始化Idris运行配置
• 创建Idris会话并加载你的Idris代码（可以是字符串或文件）
• 完成类型检查与编译
• 定位并求值指定的Idris表达式
• 将Idris的求值结果转换为Haskell可处理的数据类型

完整可运行示例 #

下面是修正并完善后的Haskell代码，它会嵌入你提供的Idris代码，求值n2并输出对应的Haskell整数：

import qualified Idris as I
import qualified Idris.Core.Evaluate as IE
import qualified Idris.Core.TT as IT
import Control.Monad.IO.Class (liftIO)

-- 修正后的Idris代码（原代码里的Nat构造器定义有误，已调整）
idrisCode :: String
idrisCode = unlines
  [ "data Nat : Type where"
  , "  Zero : Nat"
  , "  Suc : Nat -> Nat"
  , ""
  , "double : Nat -> Nat"
  , "double Zero = Zero"
  , "double (Suc n) = Suc (Suc (double n))"
  , ""
  , "n2 : Nat"
  , "n2 = double (Suc Zero)"
  ]

main :: IO ()
main = do
  -- 初始化默认Idris配置
  cfg <- I.defaultConfig
  -- 启动Idris会话并执行操作
  I.runIdris cfg $ do
    -- 加载字符串形式的Idris代码，模拟从文件加载
    I.loadString idrisCode "embedded.idr"
    -- 对所有加载的代码执行类型检查与编译
    I.checkAll
    -- 查找我们要求值的标识符"n2"
    Just n2Name <- I.getNSName "n2"
    -- 获取"n2"的定义并进行求值
    n2Def <- I.getDefinition n2Name
    let evaluatedTerm = IE.evaluate I.idrisContext (I.theDef n2Def)
    -- 把Idris的Nat类型转换为Haskell的Int（方便输出）
    let natToInt :: IT.Term -> Int
        natToInt IT.Zero = 0
        natToInt (IT.App (IT.Con _ _) arg) = 1 + natToInt arg
        natToInt _ = error "Unexpected term structure"
    -- 打印最终结果
    liftIO $ putStrLn $ "Evaluated n2: " ++ show (natToInt evaluatedTerm)

关键注意事项 #

• 依赖安装：确保你的Haskell项目依赖了idris包——用Cabal的话就在.cabal文件里加build-depends: idris，用Stack就在stack.yaml里指定对应版本。
• 代码修正：你原示例里的Nat构造器定义写错了！Zero : Nat -> Nat是错误的，正确的应该是Zero : Nat，Suc : Nat -> Nat，不然Idris会直接类型检查失败，我已经在示例里修正了这个问题。
• API稳定性：要注意，Idris的内部Haskell API没有版本稳定性承诺，不同Idris版本可能会有API变动，所以如果遇到编译错误，最好对应着你使用的Idris版本去翻源码调整。
• 错误处理：示例里简化了错误处理（比如直接用Just n2Name），实际项目里一定要处理Nothing的情况——比如Idris代码里没定义n2，或者名称拼写错误的情况。

进阶玩法 #

如果需要更复杂的交互（比如从Haskell传值给Idris，或者把Idris的复杂类型转换为Haskell类型），可以深入研究Idris.Core.TT模块里的Term类型，学习如何在两种语言的类型系统之间转换；另外，Idris.Interaction模块提供了更多会话交互函数，比如执行Idris命令、获取表达式类型等。

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