可以将Agda用作库吗？

Question

除了在文件系统上使用Agda (通过EMACS、终端等)，是否可以直接从Haskell中将其用作库？例如：

-- UsingAgda.hs
import Agda

-- Prints the type of a term on some Agda code
main :: IO ()
main = typeOf "true" agdaCode where

  agdaCode :: String
  agdaCode = unlines
    ["module Hello where   "
    ,"                     "
    ,"data Bool : Set where"
    ,"  true  : Bool       "
    ,"  false : Bool       "]

上面的代码将输出Bool，因为该Agda代码上的true : Bool。

Answer 1

是的，这是可能的。Agda被设计为一个Haskell库外加一个主模块。

你可以在here上看到几个小例子。作为一个更大的例子，我编写了Apia (无耻插件)，它使用Agda作为库。

请记住，当前的Agda description表示：

请注意，Agda包不遵循包版本控制策略，因为它不打算由第三方包使用。

当然，这是可以改变的。