是否可以使用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,因为true : Bool在那个Agda代码上.

Answer 1

对的,这是可能的.Agda被设计为Haskell库和主模块.

你可以在这里看到一些小例子.作为一个更大的例子,我写了Apia(无耻插件),它使用Agda作为库.

请记住,目前的 Agda 描述说:

请注意,Agda程序包不遵循程序包版本控制策略,因为它不适合第三方程序包使用.

当然,它可能会改变.