Как создать блок 'do' в Agda - PullRequest
Новая
       28

Как создать блок 'do' в Agda

1 голос
/ 14 апреля 2019

У меня есть код, работающий на Haskell, и я хочу преобразовать его в Agda.

Это код Haskell 

main = do
  putStrLn "A string"
  putStrLn "second string"

и вывод 

A string
second string

Я пытался преобразовать его в Agda с 

open import Common.IO

main = do
  putStrLn "A string"
  putStrLn "second string"

но я просто получаю сообщение об ошибке 

'_>>_ needs to be in scope to desugar 'do' block'

(скриншот ошибки полностью: https://imgur.com/a/3lxdwR7)

Редактировать: Это мое лучшее предположение, оно, очевидно, не сработает, но я новичок в Агде ... есть идеи? 

open import Common.IO

_>>_ : ? → ? → ?
??? = ???
??? = ???

main = do
  putStrLn "A string"
  putStrLn "second string"

... как мне заставить мой код работать в Agda?

1 Ответ

4 голосов
/ 18 апреля 2019

Я не знаю, что такое Common.IO.Используя стандартную библиотеку, вы можете написать: 

open import IO
open import Codata.Musical.Notation

main = run do
  ♯ putStrLn "A string"
  ♯ putStrLn "second string"

Забавный ♯_ - это то, что мы называем музыкальной нотацией: IO приводит к потенциально бесконечным вычислениям, поэтому мы должны использовать коиндуктивные типы.

Обратите внимание, однако, что IO в стандартной библиотеке был создан до того, как нотации были добавлены в Agda, поэтому, если они в некотором роде совместимы, это только случайно.Вероятно, лучше придерживаться >> = (и попытаться написать чистый код как можно скорее, используя только IO на границах).

...