module Revise.InfIO where
open import Coinduction open import Data.Unit open import Data.String open import Data.Colist open import Function import IO.Primitive as Prim open import Level --import IO
One cannot write "infinitely large" computations with the IO monad in IO.Primitive.
The following coinductive type is introduced to avoid this problem.
infixl 1 _>>=_ _>>_
data IO {a} (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
IOWe can now construct I/O computations with arbitrary many primitive operations, but how can we run it?
The run function does the job.
abstract
{-# 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₂)
We had to turn off the Agda termintation checker, so non-termination may present in run so we had to be careful in the implementation. (Lot better than to be careful in each individual cases!)
The use of abstract ensures that the run function will not be unfolded infinitely by the type checker.
sequence : ∀ {a} {A : Set a} → Colist (IO A) → IO (Colist A)
sequence [] = return []
sequence (c ∷ cs) = ♯ c >>= λ x →
♯ (♯ 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′ : ∀ {a} {A : Set a} → Colist (IO A) → IO (Lift ⊤)
sequence′ [] = return _
sequence′ (c ∷ cs) = ♯ c >>
♯ (♯ sequence′ (♭ cs) >>
♯ return _)
mapM : ∀ {a b} {A : Set a} {B : Set b} →
(A → IO B) → Colist A → IO (Colist B)
mapM f = sequence ∘ map f
mapM′ : {A B : Set} → (A → IO B) → Colist A → IO (Lift ⊤)
mapM′ f = sequence′ ∘ map f
------------------------------------------------------------------------
-- Simple lazy IO
getContents : IO Costring
getContents = lift Prim.getContents
readFile : String → IO Costring
readFile f = lift (Prim.readFile f)
-- Reads a finite file. Raises an exception if the file path refers to
-- a non-physical file (like "/dev/zero").
readFiniteFile : String → IO String
readFiniteFile f = lift (Prim.readFiniteFile f)
writeFile∞ : String → Costring → IO ⊤
writeFile∞ f s =
♯ lift (Prim.writeFile f s) >>
♯ return _
writeFile : String → String → IO ⊤
writeFile f s = writeFile∞ f (toCostring s)
appendFile∞ : String → Costring → IO ⊤
appendFile∞ f s =
♯ lift (Prim.appendFile f s) >>
♯ return _
appendFile : String → String → IO ⊤
appendFile f s = appendFile∞ f (toCostring s)
putStr∞ : Costring → IO ⊤
putStr∞ s =
♯ lift (Prim.putStr s) >>
♯ return _
putStr : String → IO ⊤
putStr s = putStr∞ (toCostring s)
putStrLn∞ : Costring → IO ⊤
putStrLn∞ s =
♯ lift (Prim.putStrLn s) >>
♯ return _
putStrLn : String → IO ⊤
putStrLn s = putStrLn∞ (toCostring s)