CODEWITHSUNDEEP
agda
Adjam
Adjam

Reputation: 640

How to create a 'do' block in Agda

I have some code working in Haskell and I want to convert it into Agda.

This is the Haskell code

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

and the output is

A string
second string

I've tried converting it into Agda with

open import Common.IO

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

but I just get the error message 

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

(a screenshot of the error in full: https://i.sstatic.net/pS3Ty.jpg)

Edit: This is my best guess, it obviously won't work, but I'm new to Agda... any ideas?

open import Common.IO

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

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

... how do I get my code working in Agda?

Upvotes: 5

Views: 320

Answers (1)

gallais
gallais

Reputation: 12103

I don't know what Common.IO is. Using the standard library, you can write:

open import IO
open import Codata.Musical.Notation

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

The funny ♯_ is what we call musical notation: IO leads to potentially infinite computations so we have to use coinductive types.

Note however that IO in the standard library was created before do notations were added to Agda so if they're sort-of compatible it's only by accident. It's probably better to stick to >>= (and try to write pure code as soon as possible, only using IO at the boundaries).

Upvotes: 4

Related Questions