Hyperfunctions experiment

Hyper.hs

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PostfixOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- | Hyperfunctions
-- 
-- Directly copied and adapted from https://doisinkidney.com/posts/2025-11-18-hyperfunctions.html
-- Errors and omissions are mine :)
module Exalt.Hyper where

import Control.Monad (forever)
import Control.Monad.Cont (MonadCont (callCC))
import Control.Monad.Trans (MonadIO, MonadTrans, liftIO)
import Control.Monad.Writer (MonadWriter (..), Writer, lift)
import Data.Kind (Type)
import Data.Semilattice.Join (Join, (\/))
import Data.Semilattice.Lower (Lower, lowerBound)
import Data.Void (Void, absurd)
import Debug.Trace (trace)
import Numeric.Natural (Natural)
import Prelude hiding ((||))

-- hyperfunction
newtype a :-> b = Hyper {hyp :: (b :-> a) -> b}

infixr 0 :->

konst :: b -> (a :-> b)
konst x = Hyper $ const x

-- natural numbers as a data type
data N = Z | S N

fold :: N -> (a -> a) -> a -> a
fold Z _ z = z
fold (S n) s z = s (fold n s z)

-- church encoding of natural numbers
newtype NC = NC {nat :: forall r. (r -> r) -> r -> r}

instance Show NC where
  show (NC n) = show $ n (+ 1) 0

church :: N -> NC
church n = NC $ \s z -> fold n s z

nat' :: Natural -> N
nat' 0 = Z
nat' n = S $ nat' (n - 1)

church' :: Natural -> NC
church' = church . nat'

-- standard recursive definition of less than or equal
lte :: N -> N -> Bool
lte Z _ = True
lte (S _) Z = False
lte (S n) (S m) = lte n m

-- less than or equal using hyperfunctions and church numerals
(<=?) :: NC -> NC -> Bool
n <=? m =
  hyp (nat n ns nz) (nat m ms mz)
  where
    ns :: (Bool :-> Bool) -> Bool :-> Bool
    ns mk = Hyper $ \nk -> hyp nk mk

    ms :: (Bool :-> Bool) -> Bool :-> Bool
    ms nk = Hyper $ \mk -> hyp mk nk

    nz :: Bool :-> Bool
    nz = konst True

    mz :: Bool :-> Bool
    mz = konst False

-- substraction

rep :: (a -> b) -> (a :-> b)
rep f = f <| rep f

-- "stream" of functions constructora
(<|) :: (a -> b) -> (a :-> b) -> (a :-> b)
f <| h = Hyper $ \k -> f (hyp k h)

-- zip together two streams of functions (represented as hyperfunctions)
(<.>) :: (b :-> c) -> (a :-> b) -> (a :-> c)
f <.> g = Hyper $ \h -> hyp f (g <.> h)

-- "fold" a stream of functions to a value
run :: (a :-> a) -> a
run h = hyp h (Hyper run)

-- | Subtraction of church numerals using hyperfunctions
--
-- * zip together two streams of functions representing the two numbers to be subtracted
-- * the first (finite) part of the stream consists in n (Resp. m) applications of the identity function
-- * the second (infinite) part of the stream consists in either constant zero (for n) or constant successor (for m)
-- * hence zipping the two streams results in a stream of functions that first apply identity min(n,m) times
--   and then apply either constant zero (if n <= m) or constant successor (if n > m)
(-|) :: NC -> NC -> NC
n -| m =
  NC $
    \s z ->
      run
        ( nat n ids (rep (const z))
            <.> nat m ids (rep s)
        )
  where
    ids = (id <|)

-- * Basic Message passing

type Consumer input r = r :-> (input -> r)

cons :: (input -> r -> r) -> Consumer input r -> Consumer input r
cons f c = Hyper $ \q i -> f i (hyp q c)

type Producer output r = (output -> r) :-> r

prod :: output -> Producer output r -> Producer output r
prod o p = Hyper $ \q -> hyp q p o

exec :: Producer output r -> Consumer output r -> r
exec = hyp

-- same logic as `(<=?)` but for zipping two lists: it alternates
-- between the two lists until it reaches the end of either one then
-- constantly returns the empty list
zip :: forall a b. [a] -> [b] -> [(a, b)]
zip xs ys = exec (foldr xf xb xs) (foldr yf yb ys)
  where
    xf :: a -> Producer a [(a, b)] -> Producer a [(a, b)]

    xb = konst []

    yf :: b -> Consumer a [(a, b)] -> Consumer a [(a, b)]

    yb :: Consumer a [(a, b)]
    yb = konst (const [])
    xf = prod
    yf y = cons (\x pairs -> (x, y) : pairs)

-- * CCS

data Act n = Tau | Rcv n | Snd n
  deriving (Eq, Show)

infixr 8 :·

data P n
  = (:·) (Act n) (P n) -- sequence
  | End -- termination
  | (:+) (P n) (P n) -- non deterministic choice
  | (:|) (P n) (P n) -- parallel
  | New n (P n) -- name restriction
  | Rep (P n) -- duplication
  deriving (Eq, Show)

-- An algebra to capture denotational semantics of CCS expressions of type `P n`
class CCSAlg c where
  -- | The type of names of this interpretation
  type Name c :: Type

  -- | interpret sequences
  (·) :: Act (Name c) -> c -> c

  -- | interpret termination
  end :: c

  -- | interpret non-determinism
  (⊕) :: c -> c -> c

  -- | interpret parallelism
  (||) :: c -> c -> c

  -- | Interpret name restriction
  new :: Name c -> c -> c

  -- | Repetition
  (!) :: c -> c

interpret :: (CCSAlg c) => P (Name c) -> c
interpret = \case
  a :· p -> a · interpret p
  End -> end
  p :+ q -> interpret p ⊕ interpret q
  p :| q -> interpret p || interpret q
  New n p -> new n (interpret p)
  Rep p -> (interpret p !)

-- Hyperfunctions model of CCS

type Communicator n r = (Message n -> r) :-> (Message n -> r)

data Message n = Q | A (Act n)

interp :: (CCSAlg r, n ~ Name r) => Communicator n r -> r
interp p = hyp p one Q

one :: (CCSAlg r, n ~ Name r) => Communicator n r
one = Hyper $ \p -> \case
  A a -> a · interp p
  Q -> end

instance (Eq n, Join r, Lower r) => CCSAlg (Communicator n r) where
  type Name (Communicator n r) = n
  a · p =
    Hyper $ \q m ->
      case (a, m) of
        (_, Q) -> hyp q p (A a)
        (Snd n, A (Rcv n')) | n == n' -> hyp q p (A Tau)
        _ -> lowerBound -- FIXME: should be the bottom of a semilattice?
  end = konst lowerBound
  p ⊕ q = Hyper $ \r m -> hyp p r m \/ hyp q r m
  p || q = par p q ⊕ par q p
  new n p =
    Hyper $ \q -> \case
      A Rcv {} -> lowerBound
      A Snd {} -> lowerBound
      m -> hyp p (new n q) m
  (!) p = p `par` (p !)

par :: (CCSAlg (b :-> a)) => (a :-> b) -> (b :-> a) -> a :-> b
par p q = Hyper $ \r -> hyp p (q || r)

-- denotational model representing processes as rose trees where nodes
-- are actions
newtype Proc n = Proc {root :: [(Act n, Proc n)]}
  deriving (Show)

instance (Eq n) => Join (Proc n) where
  (\/) = (⊕)

instance Lower (Proc n) where
  lowerBound = Proc []

interp' :: (CCSAlg c) => Proc (Name c) -> c
interp' (Proc []) = end
interp' (Proc ((a, p) : q)) = a · interp' p ⊕ interp' (Proc q)

instance (Eq n) => CCSAlg (Proc n) where
  type Name (Proc n) = n

  a · p = Proc [(a, p)]
  end = Proc []
  p ⊕ q = Proc (root p <> root q)
  p || q = par' p q ⊕ par' q p
  new n p =
    Proc
      [ (a, new n p')
        | (a, p') <- root p,
          a /= Rcv n,
          a /= Snd n
      ]
  (!) p = step (p ⊕ sync p p) (p !)

par' :: (Eq n) => Proc n -> Proc n -> Proc n
par' p q = sync p q ⊕ step p q

step :: (Eq n) => Proc n -> Proc n -> Proc n
step p q = Proc [(a, p' || q) | (a, p') <- root p]

sync :: (Eq n) => Proc n -> Proc n -> Proc n
sync p q =
  Proc [(Tau, p' || q') | (Rcv n, p') <- root p, (Snd n', q') <- root q, n == n']

pr :: P String
pr = (Rcv "a" :· Rcv "b" :· End) :| (Snd "a" :· End)

-- interpret pr :: Proc String
it :: Proc String
it =
  Proc
    { root =
        [ (Tau, Proc {root = [(Rcv "b", Proc {root = []})]}),
          ( Rcv "a",
            Proc
              { root =
                  [ (Rcv "b", Proc {root = [(Snd "a", Proc {root = []})]}),
                    (Snd "a", Proc {root = [(Rcv "b", Proc {root = []})]})
                  ]
              }
          ),
          ( Snd "a",
            Proc
              { root =
                  [ (Rcv "a", Proc {root = [(Rcv "b", Proc {root = []})]})
                  ]
              }
          )
        ]
    }

-- * LogicT monda

-- hyperfunction based interleaving of two lists
interleave :: [a] -> [a] -> [a]
interleave xs ys = hyp xz yz
  where
    xz = foldr (\x xk -> (x :) <| xk) (Hyper (const [])) xs
    yz = foldr (\y yk -> (y :) <| yk) (Hyper (const [])) ys

-- LogicT is a CPS-encoded list transformer
-- first arg is cons, second arg is nil
newtype LogicT m a = LogicT {runLogicT :: forall b. (a -> m b -> m b) -> m b -> m b}

evalLogicT :: (Applicative m) => LogicT m a -> m [a]
evalLogicT ls = runLogicT ls (\c -> fmap (c :)) (pure [])

(<<|) :: (Monad m) => (m b -> a) -> m (m b :-> a) -> m b :-> a
f <<| h = Hyper $ \k -> f (h >>= hyp k)

-- * Continuation based concurrency

type C m = Cont (Action m)

newtype Cont r a = Cont {runCont :: (a -> r) -> r}

instance Functor (Cont r) where
  f `fmap` (Cont k) = Cont $ \g -> k (g . f)

instance Applicative (Cont r) where
  pure a = Cont $ \k -> k a
  Cont f <*> Cont a = Cont $ \k -> f (\g -> a (k . g))

instance Monad (Cont r) where
  return = pure
  Cont m >>= f = Cont $ \k ->
    m
      ( \a -> case f a of
          Cont g -> g k
      )

instance MonadCont (Cont r) where
  callCC f = Cont $ \k -> runCont (f $ \x -> Cont $ \_ -> k x) k

data Action m = Atom (m (Action m)) | Fork (Action m) (Action m) | Stop

atom :: (Functor m) => m a -> Cont (Action m) a
atom m = Cont $ \k -> Atom (k <$> m)

fork :: (Monad m) => C m a -> Cont (Action m) ()
fork m = Cont $ \k -> Fork (action m) (k ())

action :: (Monad m) => C m a -> Action m
action (Cont f) = Atom $ return $ f (const Stop)

prog :: C (Writer String) ()
prog = do
  atom (tell "go!")
  fork (forever $ atom (tell "to"))
  forever $ atom (tell "fro")

runC :: (Monad m) => C m a -> m ()
runC p = roundC [action p]

-- round-robin scheduling of Actions
roundC :: (Monad m) => [Action m] -> m ()
roundC [] = return ()
roundC (a : as) = case a of
  Atom ma -> ma >>= \b -> roundC (as <> [b])
  Fork b b' -> roundC (as <> [b, b'])
  Stop -> roundC as

prog' :: C IO ()
prog' = do
  atom $ putStrLn "foo"
  fork (forever $ atom (putStrLn "to"))
  forever $ atom (putStrLn "fro")

-- * Concurrency monad based on hyperfunctions

-- FIXME: can't make it work
type Conc r m = Cont (m r :-> m r)

atom_h :: (Monad m) => m a -> Conc r m a
atom_h a = Cont $ \k -> id <<| (k <$> a)

fork_h :: forall r m a. Conc r m a -> Conc r m ()
fork_h m = Cont $ \k ->
  let k' = k ()
      m' = runCont m
   in m' $ const k'

-- run_h :: Conc r m a -> m ()
-- run_h c = runC (runCont c _hole)

-- * Pipes

-- similar to Gonzales' `pipes` library
newtype Pipe r i o m a = MkPipe {unPipe :: (a -> Result (m r) i o) -> Result (m r) i o}

type Result r i o = Producer i r -> Consumer o r -> r

instance Functor (Pipe r i o m) where
  f `fmap` (MkPipe k) = MkPipe $ \g -> k (g . f)

instance Applicative (Pipe r i o m) where
  pure a = MkPipe $ \k -> k a
  MkPipe f <*> MkPipe a = MkPipe $ \k -> f (\g -> a (k . g))

instance Monad (Pipe r i o m) where
  return = pure
  MkPipe m >>= f = MkPipe $ \k ->
    m
      ( \a -> case f a of
          MkPipe g -> g k
      )

instance MonadTrans (Pipe r i o) where
  lift m = MkPipe $ \k p c -> m >>= \m' -> k m' p c

-- producer side of a pipe, producing a value of type o
yield :: o -> Pipe r i o m ()
yield o = MkPipe $ \k p c -> hyp c (Hyper (k () p)) o

-- consumer side of a pipe, awaiting a value of type `i` from a symmetric `yield`
await :: Pipe r i o m i
await = MkPipe $ \k p c -> hyp p (Hyper (\p' x -> k x p' c))

-- terminates a pipe, returning some action producing a result of type `r`
halt :: m r -> Pipe r i o m x
halt x = MkPipe $ \_ _ _ -> x

-- "merges" 2 compatible pipes, a consumer side and a producer side, yielding
-- another pipe
merge :: Pipe r i x m Void -> Pipe r x o m Void -> Pipe r i o m a
merge ix xo =
  MkPipe $ \_a p c ->
    -- FIXME: action a is not evaluated meaning the last action in a pipe
    -- is ignored
    let c' = unPipe ix absurd p
        p' = unPipe xo absurd (Hyper c')
     in p' c

runPipe :: Pipe r () () m () -> m r
runPipe xs = unPipe xs h hk hc
  where
    h = const hyp
    hk = rep (\k -> k ())
    hc = rep const

instance (MonadIO m) => MonadIO (Pipe r i o m) where
  liftIO = lift . liftIO

lhs :: Pipe () () Int IO Void
lhs = do
  liftIO (putStrLn "Entered lhs")
  liftIO $ putStrLn "(1) yield 1"
  yield 1
  liftIO $ putStrLn "(1) yield 2"
  yield 2
  halt (putStrLn $ "Halt 1")

rhs :: Pipe () Int Int IO Void
rhs = do
  liftIO (putStrLn "Entered rhs")
  x <- await
  liftIO $ putStrLn $ "(2) received " <> show x
  yield $ x + 1
  y <- await
  liftIO $ putStrLn $ "(2) received " <> show y
  yield $ x + 2
  halt (putStrLn $ "Halt 2")

rrhs :: Pipe () Int () IO Void
rrhs = do
  x <- await
  liftIO $ putStrLn $ "(3) received " <> show x
  y <- await
  liftIO $ putStrLn $ "(3) received " <> show y
  halt (putStrLn $ "Halt 3")

-- * Coroutines

type Channel r i o = (o -> r) :-> (i -> r)

type Suspension r i o = Channel r o i -> r

newtype Co r i o m a = MkCo {route :: (a -> Channel (m r) o i -> m r) -> Channel (m r) o i -> m r}

instance Functor (Co r i o m) where
  f `fmap` (MkCo k) = MkCo $ \g -> k (g . f)

instance Applicative (Co r i o m) where
  pure a = MkCo $ \k -> k a
  MkCo f <*> MkCo a = MkCo $ \k -> f (\g -> a (k . g))

instance Monad (Co r i o m) where
  return = pure
  MkCo m >>= f = MkCo $ \k ->
    m
      ( \a -> case f a of
          MkCo g -> g k
      )

instance MonadTrans (Co r i o) where
  lift m = MkCo $ \k c -> m >>= \m' -> k m' c

instance MonadCont (Co r i o m) where
  callCC f = MkCo $ \s c ->
    route (f $ \x -> MkCo $ \_ b -> s x b) s c

yieldC :: o -> Co r i o m i
yieldC o = MkCo $ \k h -> hyp h (Hyper (flip k)) o

mergeC :: Co r i x m Void -> (x -> Co r x o m Void) -> Co r i o m a
mergeC ix xo =
  MkCo (\_ h -> route ix absurd (Hyper $ \h' x -> route (xo x) absurd (h <.> h')))

awaitC :: (MonadCont m) => Co r i o m r -> m (Either r (o, i -> Co r i o m r))
awaitC c = callCC $ \k ->
  Left
    <$> route
      c
      (\x _ -> return x)
      (Hyper (\h o -> k (Right (o, \i -> MkCo (\_ s -> hyp h s i)))))

await' :: (MonadCont m) => Co Void i o m Void -> m (o, i -> Co Void i o m Void)
await' c = either absurd id <$> awaitC c

runCo :: Co r i i m i -> m r
runCo c = route c (\ i -> pure _hole) id

-- send :: forall r i o m. (MonadCont m) => Co r i o m r -> i -> m (Either r (o, Co r i o m r))
-- send c v = callCC $ \k ->
--   Left
--     <$> hyp
--       (route c (\x -> Hyper (\_ _ -> return x)))
--       (Hyper (\r o -> k (Right (o, MkCo (\_ -> r)))))
--       v