将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值中累积的效果？

module Temp where

   open import Data.Unit
   open import IO

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

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

Answer 1

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

IO的问题在于终止检查器不能很好地发挥作用.因此{-# NON_TERMINATING #-},您不必定义每个函数,而是创建一个新的(共同的)数据类型来描述IO操作,并将所有非终止问题集中到一个函数中 - run.

run然后,该函数将高级IO类型给出的IO操作的描述转换为IO.Primitive可由运行时系统运行的实际IO操作().

这就是你的"Hello,world!" 程序应如下所示:

open import IO

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