cat in Agda using copatterns

Main.agda

{-# OPTIONS --copatterns #-}
module Main where
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600).

open import Data.Nat

open import Data.Unit
open import Data.Bool
open import Data.Char
open import Data.Maybe
open import Data.Product
open import Function
import Foreign.Haskell as Haskell
import IO.Primitive as Prim


-- like ⊤, but Set₁ instead of Set₀
record ⊤₁ : Set₁ where
  constructor tt₁

-- The IO module from stdlib is a wrapper around Prim.IO based on musical notation, plus a
-- NON_TERMINATING wrapper named run. Let's define our own wrapper using copatterns instead.
-- 
-- We cannot define our IO in terms of return and _>>=_. Those are constructors, that is, functions
-- which construct an IO value from smaller pieces, but when defining codata we must instead specify
-- the destructors, that is, functions which extract deeper pieces from an IO value.
record IO (B : Set) : Set₁ where
  coinductive
  field
    isDone : Maybe B          -- we either return a value of type B...
    step : if is-just isDone
           then ⊤₁            -- in which case there are no more steps, otherwise...
           else ∃ \A          -- there is an intermediate value of type A...
                → Prim.IO A   -- computed by the first step...
                × (A → IO B)  -- and followed by a continuation.
open IO

{-# NON_TERMINATING #-}
run : ∀ {B} → IO B → Prim.IO B
run ioB with isDone ioB | step ioB
... | just b  | _               = Prim.return b
... | nothing | (A , ioA , ccB) = Prim._>>=_ ioA (run ∘ ccB)

-- To define return, and any other function returning an IO value, we define what each
-- destructor should return on the resulting IO value.
return : ∀ {A} → A → IO A
isDone (return a) = just a
step   (return a) = tt₁

-- We can implement colists using the same "if then ⊤" trick:
record Colist (A : Set) : Set where
  coinductive
  field
    null : Bool
    head : if null then ⊤ else A
    tail : if null then ⊤ else Colist A
open Colist

-- Unfortunately I haven't figured out how to compile the above Colist to Haskell lists, so I can't
-- implement cat using (getContents >>= putStr∞). Instead, let's import getChar and putChar from
-- Haskell.
postulate
  isEOF   : Prim.IO Bool
  getChar : Prim.IO Char
  putChar : Char → Prim.IO Haskell.Unit
{-# COMPILED isEOF   System.IO.isEOF #-}
{-# COMPILED getChar getChar         #-}
{-# COMPILED putChar putChar         #-}

-- copatterns would be easier to read if they were right-aligned, but whitespace is significant.
cat : IO ⊤
isDone                                 cat              = nothing
proj₁                            (step cat)             = Bool
proj₁                     (proj₂ (step cat))            = isEOF
proj₂                     (proj₂ (step cat)) true       = return tt
isDone             (proj₂ (proj₂ (step cat)) false)     = nothing
proj₁        (step (proj₂ (proj₂ (step cat)) false))    = Haskell.Unit
proj₁ (proj₂ (step (proj₂ (proj₂ (step cat)) false)))   = Prim._>>=_ getChar putChar
proj₂ (proj₂ (step (proj₂ (proj₂ (step cat)) false))) _ = cat

main : Prim.IO ⊤
main = run cat