Store Comonad https://twitter.com/paf31/status/946229301912809472

Main.purs

module Main where

import Prelude

import Control.Comonad (class Comonad, extend, extract)
import Control.Comonad.Store (Store, store, peek, pos)
import Control.Comonad.Traced (Traced, runTraced, traced)
import Effect (Effect)
import Effect.Class.Console (log)
import Data.Array ((..), filter, length)
import Data.Foldable (for_)
import Data.Monoid.Additive (Additive(..))
import Data.Newtype (unwrap)
import Data.String.CodeUnits (fromCharArray)
import Data.Tuple (Tuple(..))
import TryPureScript (render, withConsole)

-- Cont is the "mother of all monads", since we can partially apply
--
--   (>>=) :: forall m a b. Monad m => m a -> (a -> m b) -> m b
--
-- to get a computation in the Cont monad:
--
--   ((x :: m a) >>= _) :: forall b. (a -> m b) -> m b
--                       ~ forall b. Cont (m b) a
--
-- And so we get a monad morphism 
--
--   m ~> Cont (m b)
--
-- for any choice of b.
--
-- We can also run the computation using `runCont return`:
--
--   runCont return :: forall m a. Monad m => Cont (m a) a -> m a
--
-- And so a language with support for composable continuations can
-- represent any monadic effects.
-- See blog.sigfpe.com/2008/12/mother-of-all-monads.html
--
-- What about comonads?
--
-- Well, if we partially apply `=>>` (a.k.a `extend`), we don't get
-- anything immediately useful, but instead we can uncurry it:
--
--   uncurry (=>>) :: forall w a b. Comonad w => Tuple (w a) (w a -> b) -> w b
--  
-- and now we notice that the left hand side is isomorphic to a store comonad:
--
--   uncurry (=>>) :: forall w a b. Comonad w => Store (w a) b -> w b
--
-- so our Store carries around our data structure and the function we want to
-- `extend` over it.
--
-- This gives us a comonad morphism
--
--   Store (w a) ~> w
--
-- for any choice of a.
--
-- We can also initialize a computation using `extract`, by simply storing any
-- comonadic value along with the `extract` function. Extending `extract` over
-- any value gives us back that value unchanged, according to the comonad laws.
--
-- We get a lifting operation:
--
--   store extract :: forall w a. Comonad w => w a -> Store (w a) a
--
-- This is seen to be dual to the case of Cont. If our language only offered
-- syntactic support for one comonad, we could choose Store, and recover support
-- for all comonads. 
-- 
-- So, Store is the mother of all comonads!

mom :: forall w a. Comonad w => w a -> Store (w a) a
mom = store extract

unMom :: forall w a b. Comonad w => Store (w a) b -> w b
unMom s = extend (flip peek s) (pos s)

-- We can just use the Store comonad's extend function, after a bit of unwrapping.
extendMom :: forall w a b c. Comonad w => (w b -> c) -> Store (w a) b -> Store (w a) c
extendMom f = extend (f <<< unMom)

-- Here is a small example - a glider in Conway's game of life - written using
-- the Store comonad (with a Traced comonad underneath).
initLife :: Store (Traced (Additive (Tuple Int Int)) Boolean) Boolean
initLife = mom grid where
  grid = glider <$> traced unwrap
  
  glider (Tuple 0 0) = true
  glider (Tuple 1 1) = true
  glider (Tuple 1 2) = true
  glider (Tuple 2 0) = true
  glider (Tuple 2 1) = true
  glider _ = false

stepLife :: Store (Traced (Additive (Tuple Int Int)) Boolean) Boolean -> Store (Traced (Additive (Tuple Int Int)) Boolean) Boolean
stepLife = extendMom (\w -> countAlive (length (filter identity (map (runTraced w <<< Additive) steps))) (extract w))
  where
    steps =
      [ Tuple (-1) (-1)
      , Tuple    0 (-1)
      , Tuple    1 (-1)
      , Tuple (-1) 0
      , Tuple    1 0
      , Tuple (-1) 1
      , Tuple    0 1
      , Tuple    1 1
      ]
      
    countAlive 3 false = true
    countAlive n true | n < 2 || n > 3 = false
    countAlive _ here = here

iterate :: forall a. Int -> (a -> a) -> a -> a
iterate 0 _ = identity
iterate n f = f <<< iterate (n - 1) f

test :: Int -> Traced (Additive (Tuple Int Int)) Boolean
test n = unMom $ iterate n stepLife $ initLife

main :: Effect Unit
main = render =<< withConsole do
  for_ (1..4) \n -> do
    log $ "Step " <> show n
    for_ (0..4) \i -> do
      let getAt = runTraced (test n) <<< Additive <<< Tuple i
          s = fromCharArray ((if _ then '#' else ' ') <<< getAt <$> 0..10)
      log s