Вывод программы программы 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!" 

Я заметил, что есть Haskell стиль run функция, объявленная в модуле IO Agda, но я не нашел способ сделать эту помощь.

Answer 1

систем Agda IO имеет в основном два слоя: нижний слой (IO.Primitive) просто прокси в Haskell IO, тем выше слой (IO) является оберткой построен на вершине.

Проблема с IO заключается в том, что она не очень хорошо работает с устройством проверки терминалов. Поэтому вместо того, чтобы определять каждую функцию с помощью {-# NON_TERMINATING #-}, вы создаете новый (коиндуктивный) тип данных, который описывает действия IO, и фокусирует все проблемы с потерей в одной единственной функции - run.

run функция затем просто переводит Desription действия IO, заданной на высоком уровне IO типа в фактическое действие ввода-вывода (IO.Primitive), который может быть запущен с помощью системы во время выполнения.

Вот как ваш «Привет, мир!» Программа должна выглядеть следующим образом:

open import IO 

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