io - 将 Agda 程序输出到控制台

Question

我已经使用 Agda 9 个月了。第一次，我发现自己想要“运行”(作为顶级可执行文件)一个打印字符串的 Agda 程序。叫我古装。

我可以编写一个计算字符串的程序，并让 Agda 在交互模式(或 Emacs)中向我显示字符串的值。但是字符串很长并且嵌入了换行符。我希望它实际打印出来。

相比之下，在 GHCi 中，我可以执行以下操作:

Prelude> putStrLn "hello, world!"
hello, world!

但是在 Agda 的交互模式下，我得到了这个:

Main> putStrLn "hello, world!"
.IO.♯-15
('h' .Data.Colist.Colist.∷
 .Data.Colist.♯-2 'h'
 ('e' .Data.List.List.∷
  'l' .Data.List.List.∷
  'l' .Data.List.List.∷
  'o' .Data.List.List.∷
  ',' .Data.List.List.∷
  ' ' .Data.List.List.∷
  'w' .Data.List.List.∷
  'o' .Data.List.List.∷
  'r' .Data.List.List.∷
  'l' .Data.List.List.∷
  'd' .Data.List.List.∷ '!' .Data.List.List.∷ .Data.List.List.[]))
>>
.IO.♯-16
('h' .Data.Colist.Colist.∷
 .Data.Colist.♯-2 'h'
 ('e' .Data.List.List.∷
  'l' .Data.List.List.∷
  'l' .Data.List.List.∷
  'o' .Data.List.List.∷
  ',' .Data.List.List.∷
  ' ' .Data.List.List.∷
  'w' .Data.List.List.∷
  'o' .Data.List.List.∷
  'r' .Data.List.List.∷
  'l' .Data.List.List.∷
  'd' .Data.List.List.∷ '!' .Data.List.List.∷ .Data.List.List.[]))

那么，我该如何获取如下的程序并运行它，以便观察 IO 中累积的效果？值(value)？

module Temp where

   open import Data.Unit
   open import IO

   main : IO ⊤
   main = putStrLn "Hello, world!"

我注意到有一个 Haskell 风格的 run在 Agda 的 IO 中声明的函数模块，但我还没有找到一种方法来提供帮助。

Answer 1

Agda IO 系统基本上有两层:下层(IO.Primitive)只是 Haskell IO 的代理。 ，较高层(IO)是建立在顶层的包装器。

IO 的问题在于它不能很好地与终止检查器配合使用。所以不必用 {-# NON_TERMINATING #-} 定义每个函数，您创建了一种新的(共归纳)数据类型来描述 IO 操作并将所有与非终止有关的问题集中到一个函数中 - run .
run然后函数只翻译高层 IO 给出的 IO 操作的描述。键入可以由运行时系统运行的实际 IO 操作 (IO.Primitive)。

这就是你的“你好，世界!”程序应如下所示:

open import IO

main = run (putStrLn "Hello, world!")