LensyMoore.hs

import Data.Fix
import Data.Functor.Identity
import Data.Functor.Const
import Data.Profunctor
import Control.Lens hiding (view, set)

--------------------------------------------------------------------------------

main = print $ runMoore fib (1, 0) [(), (), (), (), (), (), (), (), (), ()]

--------------------------------------------------------------------------------

class Functor f => Monoidal f where
  unital :: f ()
  combine :: (f x, f y) -> f (x, y)

class Monoidal3 f where
  unital3 :: f () () ()
  combine3 :: (f x y z, f x' y' z') -> f (x, x') (y, y') (z, z')

newtype Moore' s i o = Moore' (Lens s s o i)

instance Monoidal3 Moore' where
  unital3 :: Moore' () () ()
  unital3 = Moore' ($)
  
  combine3 :: (Moore' s i o, Moore' t i' o')-> Moore' (s, t) (i, i') (o, o')
  combine3 (Moore' m, Moore' n) = Moore' $ \f (x, x') -> 
    let g (y, y') = (set m x y, set n x' y')
     in fmap g $ f (view m x, view n x')

instance Functor (Moore' s i) where
  fmap f (Moore' m) = Moore' $ \bfi s -> m (bfi . f) s
  
instance Profunctor (Moore' s) where
  dimap f g (Moore' m) = Moore' $ \h s -> m (fmap f . h . g) s

--------------------------------------------------------------------------------

view :: Lens s t a b -> s -> a
view l s = getConst $ l Const s

set :: Lens s t a b -> s -> b -> t
set l s b = runIdentity $ l (\_ -> Identity b) s

--------------------------------------------------------------------------------

-- s × y^s => o × y^i
type Moore s i o = Lens s s o i

observe :: Moore s i o -> s -> o
observe m s = view m s

transition :: Moore s i o -> s -> i -> s
transition m s i = set m s i
  
runMoore :: Moore s i o -> s -> [i] -> [o]
runMoore _ s [] = []
runMoore m s (i:is) =
  let nextState = transition m s i 
      observation = view m s
  in observation : runMoore m nextState is
   
latchMachine :: Moore Int Int Int
latchMachine = lens id max

--------------------------------------------------------------------------------

tensor :: Moore s a b -> Moore t a' b' -> Moore (s, t) (a, a') (b, b')
tensor m n =
  let get' (s, t) = (view m s, view n t)
      set' (s, t) (a, a') = (set m s a, set n t a')
  in lens get' set'

-- Int × y^Int => Int × y^(Int × Int)
plus :: Moore Int (Int, Int) Int
plus = lens id (\_ (x, y) -> x + y)

-- Int × y^Int => Int × y^Int
delay :: Moore Int Int Int
delay = lens id (\x y -> y)

-- (Int × Int) × y^(Int × Int) => (Int × Int) × y^((Int × Int) × Int)
plusDelay :: Moore (Int, Int) ((Int, Int), Int) (Int, Int)
plusDelay = tensor plus delay

-- (Int × Int) × y^((Int × Int) × Int) => Int y^()
fibWiring :: Lens (Int, Int) ((Int, Int), Int) Int ()
fibWiring = 
  lens
    -- The delay output is the final observation:
    (\(pout, dout) -> dout)
    -- Input the plus result and the delay result back into the plus
    -- Input the plus result into the delay
    (\(pstate, dstate) () -> ((pstate, dstate), pstate))

fib :: Moore (Int, Int) () Int
fib = plusDelay . fibWiring

--------------------------------------------------------------------------------

-- (s × i) × y^s => o × y^()
type Mealy s i o = Lens (s, i) s o ()

observe' :: Mealy s i o -> (s, i) -> o
observe' m (s, i) = view m (s, i)

transition' :: Mealy s i o -> (s, i) -> s
transition' m (s, i) = set m (s, i) ()

runMealy :: Mealy s i o -> s -> [i] -> [(o, s)]
runMealy m s [] = []
runMealy m s (i:is) =
  let
    o = observe' m (s, i)
    s' = transition' m (s, i)
   in (o, s) : runMealy m s' is

counter :: Mealy () Int () 
counter = lens _ _

--------------------------------------------------------------------------------

annihilate :: (s, t) -> Moore s i o -> Mealy t o i -> void
annihilate (s, t) moore mealy = 
  let o = observe moore s
      i = observe' mealy (t, o)
      s' = transition moore s i
      t' = transition' mealy (t, o)
   in annihilate (s', t') moore mealy

annihilateM :: Monad m => ((o, i) -> m z) -> (s, t) -> Moore s i o -> Mealy t o i -> Fix m
annihilateM peek (s, t) moore mealy = Fix $
  let o = observe moore s
      i = observe' mealy (t, o)
      s' = transition moore s i
      t' = transition' mealy (t, o)
   in do
     -- Peek into the interaction at this state:
     peek (o, i)
     pure $ annihilateM peek (s', t') moore mealy