From b4c4163727dfa110a15bad8ee8c5eafcf41094d7 Mon Sep 17 00:00:00 2001 From: Dmitry Malikov Date: Sat, 8 Jul 2017 14:51:25 +0200 Subject: [PATCH] Chapter 15: no need to have Loop in simple Process --- Chapter15/Process.idr | 2 -- 1 file changed, 2 deletions(-) diff --git a/Chapter15/Process.idr b/Chapter15/Process.idr index b974881..fda82f9 100644 --- a/Chapter15/Process.idr +++ b/Chapter15/Process.idr @@ -8,7 +8,6 @@ data Process : Type -> Type where Request : MessagePID -> Message -> Process (Maybe Nat) Respond : ((msg : Message) -> Process Nat) -> Process (Maybe Message) Spawn : Process () -> Process (Maybe MessagePID) - Loop : Inf (Process a) -> Process a Action : IO a -> Process a Pure : a -> Process a @@ -34,7 +33,6 @@ run (Respond calc) run (Spawn proc) = do Just pid <- spawn (run proc) | Nothing => pure Nothing pure (Just (MkMessage pid)) -run (Loop action) = run action run (Action act) = act run (Pure val) = pure val run (act >>= next) = do x <- run act