|
|
@@ -0,0 +1,122 @@ |
|
|
{-# 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₁ |
|
|
|
|
|
_>>=_ : ∀ {B C} → IO B → (B → IO C) → IO C |
|
|
_>>=_ {B} {C} ioB f with isDone ioB | step ioB |
|
|
... | just b | tt₁ = f b |
|
|
... | nothing | A , ioA , ccB = go |
|
|
where |
|
|
go : IO C |
|
|
isDone go = nothing |
|
|
proj₁ (step go) = A |
|
|
proj₁ (proj₂ (step go)) = ioA |
|
|
proj₂ (proj₂ (step go)) a = ccB a >>= f |
|
|
|
|
|
_>>_ : ∀ {A B} → IO A → IO B → IO B |
|
|
ioA >> ioB = ioA >>= \_ → ioB |
|
|
|
|
|
-- copatterns would be easier to read if they were right-aligned, but whitespace is significant. |
|
|
primIO : ∀ {A} → Prim.IO A → IO A |
|
|
isDone (primIO {A} ioA) = nothing |
|
|
proj₁ (step (primIO {A} ioA)) = A |
|
|
proj₁ (proj₂ (step (primIO {A} ioA))) = ioA |
|
|
proj₂ (proj₂ (step (primIO {A} ioA))) a = return a |
|
|
|
|
|
|
|
|
-- 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 #-} |
|
|
|
|
|
|
|
|
-- Constructing a recursive computation using _>>=_ and _>>_ doesn't work because agda cannot see |
|
|
-- that the computation will make progress. |
|
|
{-# NON_TERMINATING #-} |
|
|
non-terminating-cat : IO ⊤ |
|
|
non-terminating-cat = primIO isEOF >>= \eof |
|
|
→ if eof |
|
|
then return tt |
|
|
else ( primIO getChar >>= \c |
|
|
→ primIO (putChar c) |
|
|
>> non-terminating-cat |
|
|
) |
|
|
|
|
|
-- Instead, we must inline the outer _>>=_ so that the recursive call is inside a deeper piece. |
|
|
cat : IO ⊤ |
|
|
isDone cat = nothing |
|
|
proj₁ (step cat) = Bool |
|
|
proj₁ (proj₂ (step cat)) = isEOF |
|
|
proj₂ (proj₂ (step cat)) true = return tt |
|
|
proj₂ (proj₂ (step cat)) false = primIO getChar >>= \c |
|
|
→ primIO (putChar c) |
|
|
>> non-terminating-cat |
|
|
|
|
|
main : Prim.IO ⊤ |
|
|
main = run cat |
gelisam revised this gist