From Lenses to Composable Continuations, and what lies between (Bob Atkey)

FeedbackMonad.hs

-- https://www.youtube.com/watch?v=YpklMn5yNA0
{-# LANGUAGE RankNTypes, QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
import Prelude (id, (.), ($), Functor(..), (<$>), fst)
import Data.Functor.Identity (Identity(..))
import Data.Void
import Data.Bifunctor (second)

class Feedback m where
  feedback :: (s -> r) -> m s t a -> m r t a

class IxMonad m where
  return :: a -> m r r a
  (>>=) :: m r s a -> (a -> m s t b) -> m r t b
class (IxMonad m, Feedback m) => FeedbackMonad m where
  run :: m r s s -> r
map :: IxMonad m => (a -> b) -> m r s a -> m r s b
map f m = m >>= (return . f)

type Optic m s t a b = s -> m t b a


newtype L r s a = L { unL :: (a, s -> r) }
instance IxMonad L where
  return a = L (a, id)
  L (a, s2r) >>= f = L ((s2r .) <$> unL (f a))
instance Feedback L where
  feedback s2r (L (a, t2s))= L (a, s2r . t2s)
instance FeedbackMonad L where
  run (L (s, s2r)) = s2r s

init :: FeedbackMonad m => L r s a -> m r s a
init (L (a, s2r)) = feedback s2r (return a)


newtype C r s a = C { unC :: (a -> s) -> r }
instance IxMonad C where
  return a = C (\s -> s a)
  m >>= f = C (\s -> unC m (\a -> unC (f a) s))
instance Feedback C where
  feedback s2r (C ats) = C (s2r . ats)
instance FeedbackMonad C where
  run (C s2r) = s2r id

term :: FeedbackMonad m => m r s a -> C r s a
term m = C (run . (`map` m))


-- https://julesh.com/2023/01/28/geometry-of-interaction-is-the-optic-for-copointed-functors/
newtype I r s a = I { unI :: s -> (a, r) }
instance IxMonad I where
  return a = I (\s -> (a, s))
  m >>= f = I (\t -> let (a, r) = unI m s; (b, s) = unI (f a) t in (b, r))
instance Feedback I where
  feedback s2r (I tas) = I (second s2r . tas)
instance FeedbackMonad I where
  run (I s2r) = let (s, r) = s2r s in r


data FunList t b a = Done t | More a (FunList (b -> t) b a)

tmap :: (s -> t) -> FunList s b a -> FunList t b a
tmap f (Done t) = Done (f t)
tmap f (More a z) = More a (tmap (f .) z)

ap :: FunList s b a -> FunList (s -> r) b a -> FunList r b a
Done b   `ap` c = tmap ($ b) c
More a z `ap` c = More a (z `ap` ((.) `tmap` c))

instance IxMonad FunList where
  return a = More a (Done id)
  Done t >>= _ = Done t
  More a t >>= f = f a `ap` (t >>= f)
instance Feedback FunList where
  feedback = tmap
instance FeedbackMonad FunList where
  run (Done t) = t
  run (More a fs) = run fs a


-- VL is not isomorphic to C, except when c implies f a -> a
newtype VL c t b a = VL { unVL :: forall f. c f => (a -> f b) -> f t }
instance IxMonad (VL c) where
  return a = VL (\f -> f a)
  VL t >>= f = VL (\g -> t (\a -> unVL (f a) g))
instance (forall f. c f => Functor f) => Feedback (VL c) where
  feedback s2r (VL ats) = VL (fmap s2r . ats)
instance (c Identity, forall f. c f => Functor f) => FeedbackMonad (VL c) where
  run (VL t) = runIdentity (t Identity)


-- VL is a variation on C, VLL is this same variation applied to L.
newtype VLL c t b a = VLL { unVLL :: forall f. c f => (a, f b -> f t) }
-- But it's isomorphic to L.
toL :: c Identity => VLL c r s a -> L r s a
toL (VLL (a, s2r)) = L (a, runIdentity . s2r . Identity)
instance IxMonad (VLL c) where
  return a = VLL (a, id)
  m >>= f = VLL (case m of VLL (a, s2r) -> (s2r .) <$> unVLL (f a))
instance (forall f. c f => Functor f) => Feedback (VLL c) where
  feedback s2r m = VLL (case m of (VLL (a, ts)) -> (a, fmap s2r . ts))
instance (c Identity, forall f. c f => Functor f) => FeedbackMonad (VLL c) where
  run (VLL (s, s2r)) = runIdentity (s2r (Identity s))


-- The same variation applied to I, which is not isomorphic to I, except when c implies f (a, t) -> (a, f t)
newtype VLI c t b a = VLI { unVLI :: forall f. c f => f b -> (a, f t) }
instance IxMonad (VLI c) where
  return a = VLI (\s -> (a, s))
  m >>= f = VLI (\t -> let (a, r) = unVLI m s; (b, s) = unVLI (f a) t in (b, r))
instance (forall f. c f => Functor f) => Feedback (VLI c) where
  feedback s2r (VLI tas) = VLI (second (fmap s2r) . tas)
instance (c Identity, forall f. c f => Functor f) => FeedbackMonad (VLI c) where
  run (VLI s2r) = let (s, r) = s2r (Identity s) in runIdentity r



class IxComonad w where
  extract :: w r r a -> a
  (=>>) :: w r s a -> (w t s a -> b) -> w r t b
class (IxComonad w, Feedback w) => FeedbackComonad w where
  corun :: r -> w r s s
cmap :: IxComonad w => (a -> b) -> w r s a -> w r s b
cmap f w = w =>> (f . extract)

type Optic' w s t a b = w s a b -> t


newtype Grate r s a = G { unG :: (r -> s) -> a }
instance IxComonad Grate where
  extract (G s2a2b) = s2a2b id
  G s2a2b =>> f = G (\r2t -> f (G (\t2s -> s2a2b (t2s . r2t))))
instance Feedback Grate where
  feedback rs (G rta) = G (\st -> rta (st . rs))
instance FeedbackComonad Grate where
  corun s = G (\t2s -> t2s s)

cterm :: FeedbackComonad w => w r s a -> Grate r s a
cterm w = G (\rs -> extract (feedback rs w))


newtype T r s a = T { unT :: (r, s -> a) }
instance IxComonad T where
  extract (T (r, sa)) = sa r
  T (r, sa) =>> f = T (r, \t -> f (T (t, sa)))
instance Feedback T where
  feedback r2s (T (r, ta)) = T (r2s r, ta)
instance FeedbackComonad T where
  corun r = T (r, id)

cinit :: FeedbackComonad w => T r s a -> w r s a
cinit (T (r, sa)) = sa `cmap` corun r


data VLT c r s a where
  VLT :: c f => (f r, f s -> a) -> VLT c r s a
instance IxComonad (VLT c) where
  extract (VLT (r, sa)) = sa r
  VLT (r, sa) =>> f = VLT (r, \t -> f (VLT (t, sa)))
instance (forall f. c f => Functor f) => Feedback (VLT c) where
  feedback r2s (VLT (r, ta)) = VLT (fmap r2s r, ta)
instance (c Identity, forall f. c f => Functor f) => FeedbackComonad (VLT c) where
  corun r = VLT (Identity r, runIdentity)