1  {-# LANGUAGE FlexibleContexts #-}
  2  {-# LANGUAGE FlexibleInstances #-}
  3  {-# LANGUAGE LambdaCase #-}
  4  {-# LANGUAGE PostfixOperators #-}
  5  {-# LANGUAGE RankNTypes #-}
  6  {-# LANGUAGE ScopedTypeVariables #-}
  7  {-# LANGUAGE TypeFamilies #-}
  8  {-# LANGUAGE TypeOperators #-}
  9  {-# HLINT ignore "Use camelCase" #-}
 10  {-# LANGUAGE UndecidableInstances #-}
 11  {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 12  
 13  module Hyper where
 14  
 15  import Control.Monad (forever)
 16  import Control.Monad.Cont (ContT, MonadCont (callCC))
 17  import Control.Monad.Trans (MonadIO, MonadTrans, liftIO)
 18  import Control.Monad.Writer (MonadWriter (..), Writer, lift)
 19  import Data.Kind (Type)
 20  import Data.Semilattice.Join (Join, (\/))
 21  import Data.Semilattice.Lower (Lower, lowerBound)
 22  import Data.Void (Void, absurd)
 23  import Debug.Trace (trace)
 24  import Numeric.Natural (Natural)
 25  import Prelude hiding ((||))
 26  
 27  -- hyperfunction
 28  newtype a :-> b = Hyper {hyp :: (b :-> a) -> b}
 29  
 30  infixr 0 :->
 31  
 32  konst :: b -> (a :-> b)
 33  konst x = Hyper $ const x
 34  
 35  -- natural numbers as a data type
 36  data N = Z | S N
 37  
 38  fold :: N -> (a -> a) -> a -> a
 39  fold Z _ z = z
 40  fold (S n) s z = s (fold n s z)
 41  
 42  -- church encoding of natural numbers
 43  newtype NC = NC {nat :: forall r. (r -> r) -> r -> r}
 44  
 45  instance Show NC where
 46    show (NC n) = show $ n (+ 1) 0
 47  
 48  church :: N -> NC
 49  church n = NC $ \s z -> fold n s z
 50  
 51  nat' :: Natural -> N
 52  nat' 0 = Z
 53  nat' n = S $ nat' (n - 1)
 54  
 55  church' :: Natural -> NC
 56  church' = church . nat'
 57  
 58  -- standard recursive definition of less than or equal
 59  lte :: N -> N -> Bool
 60  lte Z _ = True
 61  lte (S _) Z = False
 62  lte (S n) (S m) = lte n m
 63  
 64  -- less than or equal using hyperfunctions and church numerals
 65  (<=?) :: NC -> NC -> Bool
 66  n <=? m =
 67    hyp (nat n ns nz) (nat m ms mz)
 68    where
 69      ns :: (Bool :-> Bool) -> Bool :-> Bool
 70      ns mk = Hyper $ \nk -> hyp nk mk
 71  
 72      ms :: (Bool :-> Bool) -> Bool :-> Bool
 73      ms nk = Hyper $ \mk -> hyp mk nk
 74  
 75      nz :: Bool :-> Bool
 76      nz = konst True
 77  
 78      mz :: Bool :-> Bool
 79      mz = konst False
 80  
 81  -- substraction
 82  
 83  rep :: (a -> b) -> (a :-> b)
 84  rep f = f <| rep f
 85  
 86  -- "stream" of functions constructora
 87  (<|) :: (a -> b) -> (a :-> b) -> (a :-> b)
 88  f <| h = Hyper $ \k -> f (hyp k h)
 89  
 90  -- zip together two streams of functions (represented as hyperfunctions)
 91  (<.>) :: (b :-> c) -> (a :-> b) -> (a :-> c)
 92  f <.> g = Hyper $ \h -> hyp f (g <.> h)
 93  
 94  -- "fold" a stream of functions to a value
 95  run :: (a :-> a) -> a
 96  run h = hyp h (Hyper run)
 97  
 98  -- | Subtraction of church numerals using hyperfunctions
 99  --
100  -- * zip together two streams of functions representing the two numbers to be subtracted
101  -- * the first (finite) part of the stream consists in n (Resp. m) applications of the identity function
102  -- * the second (infinite) part of the stream consists in either constant zero (for n) or constant successor (for m)
103  -- * hence zipping the two streams results in a stream of functions that first apply identity min(n,m) times
104  --   and then apply either constant zero (if n <= m) or constant successor (if n > m)
105  (-|) :: NC -> NC -> NC
106  n -| m =
107    NC $
108      \s z ->
109        run
110          ( nat n ids (rep (const z))
111              <.> nat m ids (rep s)
112          )
113    where
114      ids = (id <|)
115  
116  -- * Basic Message passing
117  
118  type Consumer input r = r :-> (input -> r)
119  
120  cons :: (input -> r -> r) -> Consumer input r -> Consumer input r
121  cons f c = Hyper $ \q i -> f i (hyp q c)
122  
123  type Producer output r = (output -> r) :-> r
124  
125  prod :: output -> Producer output r -> Producer output r
126  prod o p = Hyper $ \q -> hyp q p o
127  
128  exec :: Producer output r -> Consumer output r -> r
129  exec = hyp
130  
131  -- same logic as `(<=?)` but for zipping two lists: it alternates
132  -- between the two lists until it reaches the end of either one then
133  -- constantly returns the empty list
134  zip :: forall a b. [a] -> [b] -> [(a, b)]
135  zip xs ys = exec (foldr xf xb xs) (foldr yf yb ys)
136    where
137      xf :: a -> Producer a [(a, b)] -> Producer a [(a, b)]
138      xf = prod
139  
140      xb = konst []
141  
142      yf :: b -> Consumer a [(a, b)] -> Consumer a [(a, b)]
143      yf y = cons (\x pairs -> (x, y) : pairs)
144  
145      yb :: Consumer a [(a, b)]
146      yb = konst (const [])
147  
148  -- * CCS
149  
150  data Act n = Tau | Rcv n | Snd n
151    deriving (Eq, Show)
152  
153  infixr 8 :·
154  
155  data P n
156    = (:·) (Act n) (P n) -- sequence
157    | End -- termination
158    | (:+) (P n) (P n) -- non deterministic choice
159    | (:|) (P n) (P n) -- parallel
160    | New n (P n) -- name restriction
161    | Rep (P n) -- duplication
162    deriving (Eq, Show)
163  
164  -- An algebra to capture denotational semantics of CCS expressions of type `P n`
165  class CCSAlg c where
166    -- | The type of names of this interpretation
167    type Name c :: Type
168  
169    -- | interpret sequences
170    (·) :: Act (Name c) -> c -> c
171  
172    -- | interpret termination
173    end :: c
174  
175    -- | interpret non-determinism
176    (⊕) :: c -> c -> c
177  
178    -- | interpret parallelism
179    (||) :: c -> c -> c
180  
181    -- | Interpret name restriction
182    new :: Name c -> c -> c
183  
184    -- | Repetition
185    (!) :: c -> c
186  
187  interpret :: (CCSAlg c) => P (Name c) -> c
188  interpret = \case
189    a :· p -> a · interpret p
190    End -> end
191    p :+ q -> interpret p ⊕ interpret q
192    p :| q -> interpret p || interpret q
193    New n p -> new n (interpret p)
194    Rep p -> (interpret p !)
195  
196  -- Hyperfunctions model of CCS
197  
198  type Communicator n r = (Message n -> r) :-> (Message n -> r)
199  
200  data Message n = Q | A (Act n)
201  
202  interp :: (CCSAlg r, n ~ Name r) => Communicator n r -> r
203  interp p = hyp p one Q
204  
205  one :: (CCSAlg r, n ~ Name r) => Communicator n r
206  one = Hyper $ \p -> \case
207    A a -> a · interp p
208    Q -> end
209  
210  instance (Eq n, Join r, Lower r) => CCSAlg (Communicator n r) where
211    type Name (Communicator n r) = n
212    a · p =
213      Hyper $ \q m ->
214        case (a, m) of
215          (_, Q) -> hyp q p (A a)
216          (Snd n, A (Rcv n')) | n == n' -> hyp q p (A Tau)
217          _ -> lowerBound -- FIXME: should be the bottom of a semilattice?
218    end = konst lowerBound
219    p ⊕ q = Hyper $ \r m -> hyp p r m \/ hyp q r m
220    p || q = par p q ⊕ par q p
221    new n p =
222      Hyper $ \q -> \case
223        A Rcv {} -> lowerBound
224        A Snd {} -> lowerBound
225        m -> hyp p (new n q) m
226    (!) p = p `par` (p !)
227  
228  par :: (CCSAlg (b :-> a)) => (a :-> b) -> (b :-> a) -> a :-> b
229  par p q = Hyper $ \r -> hyp p (q || r)
230  
231  -- denotational model representing processes as rose trees where nodes
232  -- are actions
233  newtype Proc n = Proc {root :: [(Act n, Proc n)]}
234    deriving (Show)
235  
236  instance (Eq n) => Join (Proc n) where
237    (\/) = (⊕)
238  
239  instance Lower (Proc n) where
240    lowerBound = Proc []
241  
242  interp' :: (CCSAlg c) => Proc (Name c) -> c
243  interp' (Proc []) = end
244  interp' (Proc ((a, p) : q)) = a · interp' p ⊕ interp' (Proc q)
245  
246  instance (Eq n) => CCSAlg (Proc n) where
247    type Name (Proc n) = n
248  
249    a · p = Proc [(a, p)]
250    end = Proc []
251    p ⊕ q = Proc (root p <> root q)
252    p || q = par' p q ⊕ par' q p
253    new n p =
254      Proc
255        [ (a, new n p')
256          | (a, p') <- root p,
257            a /= Rcv n,
258            a /= Snd n
259        ]
260    (!) p = step (p ⊕ sync p p) (p !)
261  
262  par' :: (Eq n) => Proc n -> Proc n -> Proc n
263  par' p q = sync p q ⊕ step p q
264  
265  step :: (Eq n) => Proc n -> Proc n -> Proc n
266  step p q = Proc [(a, p' || q) | (a, p') <- root p]
267  
268  sync :: (Eq n) => Proc n -> Proc n -> Proc n
269  sync p q =
270    Proc [(Tau, p' || q') | (Rcv n, p') <- root p, (Snd n', q') <- root q, n == n']
271  
272  pr :: P String
273  pr = (Rcv "a" :· Rcv "b" :· End) :| (Snd "a" :· End)
274  
275  -- interpret pr :: Proc String
276  it :: Proc String
277  it =
278    Proc
279      { root =
280          [ (Tau, Proc {root = [(Rcv "b", Proc {root = []})]}),
281            ( Rcv "a",
282              Proc
283                { root =
284                    [ (Rcv "b", Proc {root = [(Snd "a", Proc {root = []})]}),
285                      (Snd "a", Proc {root = [(Rcv "b", Proc {root = []})]})
286                    ]
287                }
288            ),
289            ( Snd "a",
290              Proc
291                { root =
292                    [ (Rcv "a", Proc {root = [(Rcv "b", Proc {root = []})]})
293                    ]
294                }
295            )
296          ]
297      }
298  
299  -- * LogicT monda
300  
301  -- hyperfunction based interleaving of two lists
302  interleave :: [a] -> [a] -> [a]
303  interleave xs ys = hyp xz yz
304    where
305      xz = foldr (\x xk -> (x :) <| xk) (Hyper (const [])) xs
306      yz = foldr (\y yk -> (y :) <| yk) (Hyper (const [])) ys
307  
308  -- LogicT is a CPS-encoded list transformer
309  -- first arg is cons, second arg is nil
310  newtype LogicT m a = LogicT {runLogicT :: forall b. (a -> m b -> m b) -> m b -> m b}
311  
312  evalLogicT :: (Applicative m) => LogicT m a -> m [a]
313  evalLogicT ls = runLogicT ls (\c -> fmap (c :)) (pure [])
314  
315  (<<|) :: (Monad m) => (m b -> a) -> m (m b :-> a) -> m b :-> a
316  f <<| h = Hyper $ \k -> f (h >>= hyp k)
317  
318  -- * Continuation based concurrency
319  
320  newtype Cont r a = Cont {runCont :: (a -> r) -> r}
321  
322  instance Functor (Cont r) where
323    f `fmap` (Cont k) = Cont $ \g -> k (g . f)
324  
325  instance Applicative (Cont r) where
326    pure a = Cont $ \k -> k a
327    Cont f <*> Cont a = Cont $ \k -> f (\g -> a (k . g))
328  
329  instance Monad (Cont r) where
330    return = pure
331    Cont m >>= f = Cont $ \k ->
332      m
333        ( \a -> case f a of
334            Cont g -> g k
335        )
336  
337  instance MonadCont (Cont r) where
338    callCC f = Cont $ \k -> runCont (f $ \x -> Cont $ \_ -> k x) k
339  
340  data Action m = Atom (m (Action m)) | Fork (Action m) (Action m) | Stop
341  
342  type C m = Cont (Action m)
343  
344  atom :: (Functor m) => m a -> C m a
345  atom m = Cont $ \k -> Atom (k <$> m)
346  
347  fork :: (Monad m) => C m a -> C m ()
348  fork m = Cont $ \k -> Fork (action m) (k ())
349  
350  action :: (Monad m) => C m a -> Action m
351  action (Cont f) = Atom $ return $ f (const Stop)
352  
353  prog :: C (Writer String) ()
354  prog = do
355    atom (tell "go!")
356    fork (forever $ atom (tell "to"))
357    forever $ atom (tell "fro")
358  
359  -- round-robin scheduling of Actions
360  roundC :: (Monad m) => [Action m] -> m ()
361  roundC = \case
362    [] -> return ()
363    (a : as) -> case a of
364      Atom ma -> ma >>= \b -> roundC (as <> [b])
365      Fork b b' -> roundC (as <> [b, b'])
366      Stop -> roundC as
367  
368  runC :: (Monad m) => C m a -> m ()
369  runC p = roundC [action p]
370  
371  prog' :: C IO ()
372  prog' = do
373    atom $ putStrLn "foo"
374    fork (forever $ atom (putStrLn "to"))
375    forever $ atom (putStrLn "fro")
376  
377  -- * Concurrency monad based on hyperfunctions
378  
379  type Conc r m = Cont (m r :-> m r)
380  
381  atom_h :: (Monad m) => m a -> Conc r m a
382  atom_h a = Cont $ \k -> id <<| (k <$> a)
383  
384  fork_h :: forall r m a. Conc r m a -> Conc r m ()
385  fork_h m = Cont $ \k ->
386    let k' = k ()
387        m' = runCont m
388     in m' $ const k'
389  
390  run_h :: (Monad m) => Conc r m a -> m r
391  run_h c = run (runCont c (\_ -> rep id))
392  
393  prog'' :: Conc r IO b
394  prog'' = do
395    atom_h $ putStrLn "foo"
396    fork_h (forever $ atom_h (putStrLn "to"))
397    forever $ atom_h (putStrLn "fro")
398  
399  -- * Pipes
400  
401  -- similar to Gonzales' `pipes` library
402  newtype Pipe r i o m a = MkPipe {unPipe :: (a -> Result (m r) i o) -> Result (m r) i o}
403  
404  type Result r i o = Producer i r -> Consumer o r -> r
405  
406  instance Functor (Pipe r i o m) where
407    f `fmap` (MkPipe k) = MkPipe $ \g -> k (g . f)
408  
409  instance Applicative (Pipe r i o m) where
410    pure a = MkPipe $ \k -> k a
411    MkPipe f <*> MkPipe a = MkPipe $ \k -> f (\g -> a (k . g))
412  
413  instance Monad (Pipe r i o m) where
414    return = pure
415    MkPipe m >>= f = MkPipe $ \k ->
416      m
417        ( \a -> case f a of
418            MkPipe g -> g k
419        )
420  
421  instance MonadTrans (Pipe r i o) where
422    lift m = MkPipe $ \k p c -> m >>= \m' -> k m' p c
423  
424  -- producer side of a pipe, producing a value of type o
425  yield :: o -> Pipe r i o m ()
426  yield o = MkPipe $ \k p c -> hyp c (Hyper (k () p)) o
427  
428  -- consumer side of a pipe, awaiting a value of type `i` from a symmetric `yield`
429  await :: Pipe r i o m i
430  await = MkPipe $ \k p c -> hyp p (Hyper (\p' x -> k x p' c))
431  
432  -- terminates a pipe, returning some action producing a result of type `r`
433  halt :: m r -> Pipe r i o m x
434  halt x = MkPipe $ \_ _ _ -> x
435  
436  -- "merges" 2 compatible pipes, a consumer side and a producer side, yielding
437  -- another pipe
438  merge :: Pipe r i x m Void -> Pipe r x o m Void -> Pipe r i o m a
439  merge ix xo =
440    MkPipe $ \_a p c ->
441      -- FIXME: action a is not evaluated meaning the last action in a pipe
442      -- is ignored
443      let c' = unPipe ix absurd p
444          p' = unPipe xo absurd (Hyper c')
445       in p' c
446  
447  runPipe :: Pipe r () () m () -> m r
448  runPipe xs = unPipe xs h hk hc
449    where
450      h = const hyp
451      hk = rep (\k -> k ())
452      hc = rep const
453  
454  instance (MonadIO m) => MonadIO (Pipe r i o m) where
455    liftIO = lift . liftIO
456  
457  lhs :: Pipe () () Int IO Void
458  lhs = do
459    liftIO (putStrLn "Entered lhs")
460    liftIO $ putStrLn "(1) yield 1"
461    yield 1
462    liftIO $ putStrLn "(1) yield 2"
463    yield 2
464    halt (putStrLn $ "Halt 1")
465  
466  rhs :: Pipe () Int Int IO Void
467  rhs = do
468    liftIO (putStrLn "Entered rhs")
469    x <- await
470    liftIO $ putStrLn $ "(2) received " <> show x
471    yield $ x + 1
472    y <- await
473    liftIO $ putStrLn $ "(2) received " <> show y
474    yield $ x + 2
475    halt (putStrLn $ "Halt 2")
476  
477  rrhs :: Pipe () Int () IO Void
478  rrhs = do
479    x <- await
480    liftIO $ putStrLn $ "(3) received " <> show x
481    y <- await
482    liftIO $ putStrLn $ "(3) received " <> show y
483    halt (putStrLn $ "Halt 3")
484  
485  -- * Coroutines
486  
487  type Channel r i o = (o -> r) :-> (i -> r)
488  
489  type Suspension r i o = Channel r o i -> r
490  
491  newtype Co r i o m a = MkCo {route :: (a -> Channel (m r) o i -> m r) -> Channel (m r) o i -> m r}
492  
493  instance Functor (Co r i o m) where
494    f `fmap` (MkCo k) = MkCo $ \g -> k (g . f)
495  
496  instance Applicative (Co r i o m) where
497    pure a = MkCo $ \k -> k a
498    MkCo f <*> MkCo a = MkCo $ \k -> f (\g -> a (k . g))
499  
500  instance Monad (Co r i o m) where
501    return = pure
502    MkCo m >>= f = MkCo $ \k ->
503      m
504        ( \a -> case f a of
505            MkCo g -> g k
506        )
507  
508  instance MonadTrans (Co r i o) where
509    lift m = MkCo $ \k c -> m >>= \m' -> k m' c
510  
511  instance MonadCont (Co r i o m) where
512    callCC f = MkCo $ \s c ->
513      route (f $ \x -> MkCo $ \_ b -> s x b) s c
514  
515  yieldC :: o -> Co r i o m i
516  yieldC o = MkCo $ \k h -> hyp h (Hyper (flip k)) o
517  
518  mergeC :: Co r i x m Void -> (x -> Co r x o m Void) -> Co r i o m a
519  mergeC ix xo =
520    MkCo (\_ h -> route ix absurd (Hyper $ \h' x -> route (xo x) absurd (h <.> h')))
521  
522  awaitC :: (MonadCont m) => Co r i o m r -> m (Either r (o, i -> Co r i o m r))
523  awaitC c = callCC $ \k ->
524    Left
525      <$> route
526        c
527        (\x _ -> return x)
528        (Hyper (\h o -> k (Right (o, \i -> MkCo (\_ s -> hyp h s i)))))
529  
530  await' :: (MonadCont m) => Co Void i o m Void -> m (o, i -> Co Void i o m Void)
531  await' c = either absurd id <$> awaitC c
532  
533  runCo :: Co r i i m i -> m r
534  runCo c = route c idS hid
535  
536  idS :: i -> Suspension r i i
537  idS i c = hyp c hid i
538  
539  hid :: (i -> r) :-> (i -> r)
540  hid = rep id
541  
542  send :: forall m r i o. (MonadCont m) => Co r i o m r -> i -> m (Either r (o, Co r i o m r))
543  send c v = callCC $ \k ->
544    Left
545      <$> route
546        c
547        (\x _ -> return x)
548        (Hyper (\h o -> k (Right (o, MkCo (\_ s -> hyp h s v)))))
549  
550  class (Monad m) => MonadSay m where
551    say :: String -> m ()
552  
553  instance (Monad m, MonadWriter [String] m) => MonadSay m where
554    say = tell . (: [])
555  
556  gen :: (MonadSay m) => Co Void Int Int m Void
557  gen = forever $ do
558    lift $ say "in gen"
559    x <- yieldC 1
560    lift $ say $ "yielded 1, received " <> show x
561    x <- yieldC 2
562    lift $ say $ "yielded 2, received " <> show x
563    x <- yieldC 3
564    lift $ say $ "yielded 3, received " <> show x
565  
566  progC :: (MonadSay m, MonadCont m) => Co Void Int Int m Void -> m ()
567  progC g = do
568    send g 12 >>= \case
569      Left r -> say $ "coroutine done " <> show r
570      Right (x, kg) -> do
571        say "in prog"
572        (x, kg) <- await' g
573        say $ "received " <> show x
574        (x, kg) <- await' (kg 10)
575        say $ "sent 10, received " <> show x
576        (x, kg) <- await' (kg 20)
577        say $ "sent 20, received " <> show x
578        (x, kg) <- await' (kg 30)
579        say $ "sent 30, received " <> show x