CODEWITHSUNDEEP
monadsagdadependent-typecoinduction
mattdf
mattdf

Reputation: 21

Reading a string from the command line in Agda 2

How do you read string input into Agda in 2.6+?

I have been fighting to just write a program that reads a line of input and immediately spits it back. There seems to always be an issue, no matter what I try. Despite searching, I cannot find a simple example. The hello world only outputs. If I try to input and then output, then I need some kind of monad. I've tried haskell style, but that obviously won't work. I've tried using musical notation, but still doesn't do it. I'm looking for the simplest example, something with

main = do
  s <- getLine
  putStrLn s

I've tried too many variations to list, but all seem to fall prey to some issue. Even when I seem to get the monad right, it complains of trying to unify different definitions of IO. ChatGPT got all snippy and told me to try Idris if I want to write dependent code that actually does something.

Upvotes: 1

Views: 164

Answers (1)

gallais
gallais

Reputation: 12103

You're on the right track: you're only missing an import (Agda does not load anything by default) and a type annotation (Agda requires top-level annotations).

The docs have an example that can be extended to your program:

{-# OPTIONS --guardedness #-}

open import IO

main : Main
main = run do
  s <- getLine
  putStrLn s

Note that this requires the standard library being installed.

Upvotes: 2

Related Questions