如何从Agda的Haskell FFI中使用Cabal依赖？

Haskell绘图代码（Dynamical/Plot/src/HsPlot.hs） #

-- Dynamical/Plot/src/HsPlot.hs
module HsPlot where

import Graphics.Rendering.Chart.Easy
import Graphics.Rendering.Chart.Backend.Cairo

plotToFile :: Double -> [Double] -> [Double] -> IO ()
plotToFile dt r f = toFile def "plot.png" $ do
    layout_title .= "Dynamics idk"
    setColors [opaque blue, opaque red]
    plot (line "rabbits" [zip [0, dt..] r ])
    plot (line "foxes" [zip [0, dt..] f])

Agda调用代码（Dynamical/Plot/Plot.agda） #

-- Dynamical/Plot/Plot.agda
{-# OPTIONS --sized-types --guardedness #-}

module Dynamical.Plot.Plot where

open import Agda.Builtin.IO
open import Data.Float
open import Data.Unit
open import Data.List as List using (List)
open import Data.Product

postulate
  plotDynamics  : Float → List Float → List Float → IO ⊤

{-# FOREIGN GHC import HsPlot #-}
{-# COMPILE GHC plotDynamics = plotToFile #-}

open import Dynamical.LotkaVolterra
import Data.Vec as Vec

main = do
  -- lvList is a Vec of Floats, needs to be a list
  let dyn = Vec.toList lvList
  let r , f = List.unzip dyn
  plotDynamics 0.1 r f

执行命令与错误信息 #

执行的编译命令：

agda -c Dynamical/Plot/Plot.agda --ghc-flag=-iDynamical/Plot/src

出现的错误：

/Users/deco/work/poly/MAlonzo/Code/Dynamical/Plot/Plot.hs:29:1: error:
    Could not find module ‘HsPlot’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
29 | import HsPlot

项目目录结构 #

.
├── Categorical
│   ├── Adjunction.agda
│   ├── CartesianClosed.agda
│   ├── CompositionMonoid.agda
│   ├── Coproduct.agda
│   ├── CubicalPoly.agda
│   ├── Exponential.agda
│   ├── Functor
│   │   ├── Constant.agda
│   │   ├── Linear.agda
│   │   ├── PlugInOne.agda
│   │   └── PlugInZero.agda
│   ├── Gist.agda
│   ├── Initial.agda
│   ├── ParallelProductMonoid.agda
│   ├── Product.agda
│   └── Terminal.agda
├── Common
│   └── CategoryData.agda
└── Dynamical
    ├── Fibonacci.agda
    ├── HodgkinHuxley.agda
    ├── LotkaVolterra.agda
    ├── Plot
    │   ├── HsPlot.cabal
    │   ├── Plot.agda
    │   ├── hie.yaml
    │   └── src
    │       └── HsPlot.hs
    ├── System.agda
    └── Turing.agda

解决方案 #

方法一：用Cabal统一管理项目（推荐） #

将Agda和Haskell代码整合到同一个Cabal项目中，自动处理依赖与路径问题：

1. 修改HsPlot.cabal文件
   更新Dynamical/Plot/HsPlot.cabal，添加Agda编译目标：

   cabal-version: 3.0
   name: HsPlot
   version: 0.1.0.0
   license: BSD-3-Clause
   author: Your Name
   maintainer: your.email@example.com
   build-type: Simple
   
   executable plot-dynamics
     main-is: Plot.agda
     hs-source-dirs: src, .
     default-language: Haskell2010
     build-depends:
       base >=4.14 && <5,
       Chart >=1.9,
       Chart-cairo >=1.9,
       Agda >=2.6.2
     ghc-options: -i../..
     build-tool-depends: agda:agda
     other-modules:
       HsPlot
       Dynamical.LotkaVolterra
   

   • hs-source-dirs包含Haskell源码目录src和Agda文件所在的当前目录.
   • ghc-options: -i../..确保GHC能找到上层目录的Agda模块编译产物

2. 编译运行
   在Dynamical/Plot目录下执行：

   cabal build
   cabal run plot-dynamics
   

方法二：手动传递完整路径与依赖参数 #

如果不想用Cabal管理，直接通过Agda命令传递GHC所需的参数：

1. 提前安装依赖
   先确保Chart库已安装：

   cabal install Chart Chart-cairo
   

2. 修正Agda编译命令
   使用绝对路径指定Haskell源码目录，同时传递依赖包参数：

   agda -c Dynamical/Plot/Plot.agda \
     --ghc-flag=-i$(pwd)/Dynamical/Plot/src \
     --ghc-flag=-package Chart \
     --ghc-flag=-package Chart-cairo
   

   • $(pwd)获取当前目录绝对路径，避免相对路径失效问题
   • -package参数告诉GHC引入Chart相关依赖库

关键注意事项 #

• 模块路径必须明确：GHC对相对路径的解析基于Agda生成代码的临时目录，使用绝对路径更可靠
• 依赖必须显式传递：GHC不会自动读取Cabal文件，需手动指定-package参数引入第三方库
• Cabal管理更省心：长期维护项目推荐用Cabal统一管理，避免手动维护大量编译参数

内容的提问来源于stack exchange，提问作者André Muricy