Yes in Agda

yes.agda

module Yes where

open import Codata.Musical.Notation

open import Data.List using (List; []; _∷_)
open import Data.String using (String; unwords; _++_)
open import Data.Unit using (⊤)

open import Function using (case_of_)

open import IO
import IO.Primitive as Prim

postulate
  getArgs : Prim.IO (List String)
  getProgName : Prim.IO String
{-# FOREIGN GHC import qualified System.Environment as Env #-}
{-# FOREIGN GHC import qualified Data.Text as Text #-}
{-# COMPILE GHC getArgs = fmap (map Text.pack) Env.getArgs #-}
{-# COMPILE GHC getProgName = fmap Text.pack Env.getProgName #-}

help : String → String
help progName =
  "Usage: " ++ progName ++ " [STRING]...\n\
  \  or:  " ++ progName ++ " OPTION\n\
  \Repeatedly output a line with all specified STRING(s), or 'y'.\n\
  \\n\
  \--help     display this help and exit\n\
  \--version  output version information and exit"

version : String
version = "yes (Agda) 0.1"

loop : ∀ {A : Set} → String → IO A
loop str = ♯ putStrLn str >>= λ _ → ♯ loop str

main′ : IO _
main′ = ♯ lift getArgs >>= λ args → case args of λ
  { [] → ♯ loop "y"
  ; ("--help" ∷ []) → ♯ (♯ lift getProgName >>= λ progName → ♯ putStrLn (help progName))
  ; ("--version" ∷ []) → ♯ putStrLn version
  ; xs → ♯ loop (unwords xs)
  }

main : Prim.IO _
main = run main′