[ refactor ] IO module (#1364)

Author: gallais

CHANGELOG.md

@@ -59,6 +59,13 @@ Non-backwards compatible changes
   to `Data.List.Relation.Binary.BagAndSetEquality` as their current location
   were causing cyclic import dependencies.
 
+* Clean up of `IO` to make it more friendly:
+  + Renamed `_>>=_` and `_>>_` to `bind` and `seq` respectively to free up the names
+    for `do`-notation friendly combinators.
+  + Introduced `Colist` and `List` modules for the various `sequence` and `mapM` functions.
+    This breaks code that relied on the `Colist`-specific function being exported as part of `IO`.
+
+
 Deprecated modules
 ------------------
 
@@ -389,3 +396,8 @@ Other minor additions
   function : Func S S
   id-⟶     : A ⟶ A
   ```
+
+* Added new function to `Data.String.Base`:
+  ```agda
+  lines : String → List String
+  ```

README/Foreign/Haskell.agda

@@ -88,11 +88,11 @@ open import Relation.Nullary.Negation
 
 -- example program using uncons, catMaybes, and testChar
 
-main = run $
-  ♯ readFiniteFile "README/Foreign/Haskell.agda" {- read this file -} >>= λ f →
-  ♯ let chars   = toList f in
-    let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing) in
-    let cleaned = dropWhile ('\n' ≟_) $ cleanup chars in
+main = run $ do
+  content ← readFiniteFile "README/Foreign/Haskell.agda"
+  let chars = toList content
+  let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing)
+  let cleaned = dropWhile ('\n' ≟_) $ cleanup chars
   case uncons cleaned of λ where
     nothing         → putStrLn "I cannot believe this file is filed with dashes only!"
     (just (c , cs)) → putStrLn $ unlines

README/IO.agda

@@ -0,0 +1,60 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Simple examples of programs using IO
+------------------------------------------------------------------------
+
+{-# OPTIONS --guardedness #-}
+
+module README.IO where
+
+open import Data.Nat.Base
+open import Data.Nat.Show using (show)
+open import Data.String.Base using (String; lines)
+open import Function.Base using (_$_)
+open import IO
+open import System.Environment
+
+------------------------------------------------------------------------
+-- NO GUARDEDNESS
+
+-- If you do not need to rely on guardedness for the function to be seen as
+-- terminating (for instance because it is structural in an inductive argument)
+-- then you can use `do` notations to write fairly readable programs.
+
+-- Countdown to explosion
+countdown : ℕ → IO _
+countdown zero      = putStrLn "BOOM!"
+countdown m@(suc n) = do
+  let str = show m
+  putStrLn str
+  countdown n
+
+-- cat the content of a finite file
+cat : String → IO _
+cat fp = do
+  content ← readFiniteFile fp
+  let ls = lines content
+  List.mapM′ putStrLn ls
+
+open import Codata.Musical.Notation
+open import Codata.Musical.Colist
+open import Data.Bool
+open import Data.Unit.Polymorphic.Base
+
+------------------------------------------------------------------------
+-- GUARDEDNESS
+
+-- If you are performing coinduction on a potentially infinite piece of codata
+-- then you need to rely on guardedness. That is to say that the coinductive
+-- call needs to be obviously under a coinductive constructor and guarded by a
+-- sharp (♯_).
+-- In this case you cannot use the convenient combinators that make `do`-notations
+-- and have to revert back to the underlying coinductive constructors.
+
+
+-- Whether a colist is finite is semi decidable: just let the user wait until
+-- you reach the end!
+isFinite : ∀ {a} {A : Set a} → Colist A → IO Bool
+isFinite []       = return true
+isFinite (x ∷ xs) = seq (♯ return tt) (♯ isFinite (♭ xs))

src/Data/String/Base.agda

@@ -89,9 +89,6 @@ intersperse sep = concat ∘′ (List.intersperse sep)
 
 -- String-specific functions
 
-unlines : List String → String
-unlines = intersperse "\n"
-
 wordsBy : ∀ {p} {P : Pred Char p} → Decidable P → String → List String
 wordsBy P? = List.map fromList ∘ List.wordsBy P? ∘ toList
 
@@ -101,6 +98,12 @@ words = wordsBy (T? ∘ Char.isSpace)
 unwords : List String → String
 unwords = intersperse " "
 
+lines : String → List String
+lines = wordsBy ('\n' Char.≟_)
+
+unlines : List String → String
+unlines = intersperse "\n"
+
 parens : String → String
 parens s = "(" ++ s ++ ")"
 

src/IO.agda

@@ -9,14 +9,17 @@
 module IO where
 
 open import Codata.Musical.Notation
-open import Codata.Musical.Colist
 open import Codata.Musical.Costring
 open import Data.Unit.Polymorphic
 open import Data.String
 open import Function
 import IO.Primitive as Prim
 open import Level
 
+private
+  variable
+    a b : Level
+
 ------------------------------------------------------------------------
 -- The IO monad
 
@@ -27,50 +30,96 @@ open import Level
 -- introduced to avoid this problem. Possible non-termination is
 -- isolated to the run function below.
 
-infixl 1 _>>=_ _>>_
-
-data IO {a} (A : Set a) : Set (suc a) where
+data IO (A : Set a) : Set (suc a) where
   lift   : (m : Prim.IO A) → IO A
   return : (x : A) → IO A
-  _>>=_  : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
-  _>>_   : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A
+  bind   : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
+  seq    : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A
+
+pure : {A : Set a} → A → IO A
+pure = return
+
+module _ {A B : Set a} where
+
+  infixl 1 _<$>_ _<*>_ _>>=_ _>>_
+
+  _<*>_ : IO (A → B) → IO A → IO B
+  mf <*> mx = bind (♯ mf) λ f → ♯ (bind (♯ mx) λ x → ♯ pure (f x))
+
+  _<$>_ : (A → B) → IO A → IO B
+  f <$> m = pure f <*> m
+
+  _>>=_ : IO A → (A → IO B) → IO B
+  m >>= f = bind (♯ m) λ x → ♯ f x
+
+  _>>_ : IO A → IO B → IO B
+  m₁ >> m₂ = seq (♯ m₁) (♯ m₂)
 
 {-# NON_TERMINATING #-}
 
-run : ∀ {a} {A : Set a} → IO A → Prim.IO A
-run (lift m)   = m
-run (return x) = Prim.return x
-run (m  >>= f) = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x))
-run (m₁ >> m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)
+run : {A : Set a} → IO A → Prim.IO A
+run (lift m)    = m
+run (return x)  = Prim.return x
+run (bind m f)  = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x))
+run (seq m₁ m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)
 
 ------------------------------------------------------------------------
 -- Utilities
 
-sequence : ∀ {a} {A : Set a} → Colist (IO A) → IO (Colist A)
-sequence []       = return []
-sequence (c ∷ cs) = ♯ c                  >>= λ x  →
-                    ♯ (♯ sequence (♭ cs) >>= λ xs →
-                    ♯ return (x ∷ ♯ xs))
+module Colist where
+
+  open import Codata.Musical.Colist
+
+  module _  {A : Set a} where
+
+    sequence : Colist (IO A) → IO (Colist A)
+    sequence []       = return []
+    sequence (c ∷ cs) = bind (♯ c)               λ x  → ♯
+                        bind (♯ sequence (♭ cs)) λ xs → ♯
+                        return (x ∷ ♯ xs)
+
+    -- The reason for not defining sequence′ in terms of sequence is
+    -- efficiency (the unused results could cause unnecessary memory use).
+
+    sequence′ : Colist (IO A) → IO ⊤
+    sequence′ []       = return _
+    sequence′ (c ∷ cs) = seq (♯ c) (♯ sequence′ (♭ cs))
+
+  module _ {A : Set a} {B : Set b} where
+
+    mapM : (A → IO B) → Colist A → IO (Colist B)
+    mapM f = sequence ∘ map f
+
+    mapM′ : (A → IO B) → Colist A → IO ⊤
+    mapM′ f = sequence′ ∘ map f
+
+module List where
+
+  open import Data.List.Base
+
+  module _  {A : Set a} where
+
+    sequence : List (IO A) → IO (List A)
+    sequence []       = ⦇ [] ⦈
+    sequence (c ∷ cs) = ⦇ c ∷ sequence cs ⦈
 
--- The reason for not defining sequence′ in terms of sequence is
--- efficiency (the unused results could cause unnecessary memory use).
+    -- The reason for not defining sequence′ in terms of sequence is
+    -- efficiency (the unused results could cause unnecessary memory use).
 
-sequence′ : ∀ {a} {A : Set a} → Colist (IO A) → IO ⊤
-sequence′ []       = return _
-sequence′ (c ∷ cs) = ♯ c                   >>
-                     ♯ (♯ sequence′ (♭ cs) >>
-                     ♯ return _)
+    sequence′ : List (IO A) → IO ⊤
+    sequence′ []       = return _
+    sequence′ (c ∷ cs) = c >> sequence′ cs
 
-module _ {a b} {A : Set a} {B : Set b} where
+  module _ {A : Set a} {B : Set b} where
 
-  mapM : (A → IO B) → Colist A → IO (Colist B)
-  mapM f = sequence ∘ map f
+    mapM : (A → IO B) → List A → IO (List B)
+    mapM f = sequence ∘ map f
 
-  mapM′ : (A → IO B) → Colist A → IO ⊤
-  mapM′ f = sequence′ ∘ map f
+    mapM′ : (A → IO B) → List A → IO ⊤
+    mapM′ f = sequence′ ∘ map f
 
 ignore : ∀ {a} {A : Set a} → IO A → IO ⊤
-ignore io = ♯ io >> ♯ return _
+ignore io = io >> return _
 
 ------------------------------------------------------------------------
 -- Simple lazy IO