可以将Agda用作库吗?

本文介绍了可以将Agda用作库吗?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

除了可以在文件系统(带有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.

当然，它可能会改变.