Fx.idr

module Fx

-- Just playing around with implementing my own free effects system in Iris
-- while watching https://www.youtube.com/watch?v=kIwd1D9m1gE

import Data.IORef

-- ================================================================ --
-- CrapMap
-- ================================================================ --

data Map k v = MkMap (List (k, v))

(Eq k, Eq v, Ord k, Ord v) => Eq (Map k v) where
  (==) (MkMap xs) (MkMap ys) = sort xs == sort ys

empty : Map k v
empty = MkMap []

delete : (Eq k, Eq v) => k -> Map k v -> Map k v
delete k (MkMap xs) = case find ((== k) . fst) xs of
  Nothing     => MkMap xs
  Just (_, v) => MkMap $ delete (k, v) xs

insert : (Eq k, Eq v) => k -> v -> Map k v -> Map k v
insert k v m = let (MkMap xs') = delete k m in MkMap ((k, v) :: xs')

lookup : Eq k => k -> Map k v -> Maybe v
lookup x (MkMap xs) = Prelude.List.lookup x xs

-- ================================================================ --
-- Free stuff ganked from
--   https://github.com/idris-hackers/idris-free/blob/master/Control/Monad/Free.idr
-- ================================================================ --

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

Functor f => Functor (Free f) where
   map f m = assert_total $ case m of
    Pure x => Pure (f x)
    Bind x => Bind (map (map f) x)

Functor f => Applicative (Free f) where
  pure = Pure

  m <*> x = assert_total $ case m of
    Pure f => map f x
    Bind f => Bind (map (<*> x) f)

Functor f => Monad (Free f) where
  m >>= f = assert_total $ case m of
    Pure x => f x
    Bind x => Bind (map (>>= f) x)

foldFree : (Monad m, Functor f) => ({ a : Type } -> f a -> m a) -> Free f b -> m b
foldFree f m = assert_total $ case m of
  Pure x => pure x
  Bind x => f x >>= foldFree f

-- ================================================================ --
-- "Business"
-- ================================================================ --

data UUID = MkUUID Int

implementation Eq UUID where
  (==) (MkUUID a) (MkUUID b) = a == b

implementation Ord UUID where
  (>=) (MkUUID a) (MkUUID b) = a >= b
  compare (MkUUID a) (MkUUID b) = compare a b

data Storage a
  = Persist UUID Int a
  | Fetch UUID (Maybe Int -> a)

implementation Functor Storage where
  map f (Persist uuid n next) = Persist uuid n (f next)
  map f (Fetch uuid cont)     = Fetch uuid (f . cont)

persist : UUID -> Int -> Free Storage ()
persist uuid n = Bind (Persist uuid n (Pure ()))

fetch : UUID -> Free Storage (Maybe Int)
fetch uuid = Bind (Fetch uuid Pure)

interpret : IORef (Map UUID Int) -> Storage a -> IO a
interpret ref (Persist uuid n next) = do
  modifyIORef ref (insert uuid n)
  pure next
interpret ref (Fetch uuid cont) = do
  storage <- readIORef ref
  pure $ cont $ Fx.lookup uuid storage

emptyStorageMap : Map UUID Int
emptyStorageMap = empty

doStuff : UUID -> Int -> Free Storage String
doStuff uuid n = do
  oldMay <- fetch uuid
  let oldN = fromMaybe 0 oldMay
  let newN = oldN + n
  persist uuid newN
  pure $ "New value: " ++ show newN

void_ : Monad m => m a -> m ()
void_ = (*> pure ())

main : IO ()
main = do
  ref <- newIORef empty
  void_ . foldFree (interpret ref) $ doStuff (MkUUID 5) 10