可以将Agda用作库吗? [英] Is it possible to use Agda as a library?

问题描述

除了可以在文件系统(带有EMACS，终端等)上使用Agda之外，还可以直接从Haskell作为库使用它吗?例如:

Instead of using Agda on a filesystem (with EMACS, terminal, etc.), is it possible to use it directly from Haskell, as a library? For example:

-- 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.

The code above would output Bool, because true : Bool on that Agda code.

推荐答案

是的，有可能. Agda被设计为Haskell库和一个主要模块.

Yes, it is possible. Agda was designed as a Haskell library plus a main module.

您可以在此处看到几个小示例.作为一个更大的例子，我写了 Apia (无耻插件)，它使用Agda作为库.

You can see a couple of small examples here. As a bigger example, I wrote Apia (shameless plug), which uses Agda as a library.

请记住，当前 Agda 说明说:

Please keep in mind that the current Agda description says:

请注意，Agda软件包不遵循软件包版本控制 政策，因为它不打算由第三方程序包使用.

Note that the Agda package does not follow the package versioning policy, because it is not intended to be used by third-party packages.

当然，它可能会改变.

这篇关于可以将Agda用作库吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！