open import Prelude

{- Modeling Redis

   Redis is an in-memory key-value datastore. It is essentially a hash
   table with several built-in primitive value types.

   From Redis's perspective, we're given access to some low-level
   commands to store and retrieve data. The full list is documented
   at http://redis.io/commands.

   In this article, I will demonstrate how to construct a high-level,
   type-safe abstraction over Redis's low-level commands via the Free
   monad.

   So without further ado, here are some of Redis's low-level commands:

-}

RedisPrimitiveCommand = IO

postulate
  -- simple key-value access commands
  GET : (key : String) → RedisPrimitiveCommand (Maybe String)
  SET : (key value : String) → RedisPrimitiveCommand ⊤
  DELETE : (key : String) → RedisPrimitiveCommand ⊤

  -- access commands for values in a built-in Redis list
  GETLIST : (key : String) → RedisPrimitiveCommand (List String)
  PREPEND : (key value : String) → RedisPrimitiveCommand ⊤

-- example usage

setHelloWorld : RedisPrimitiveCommand ⊤
setHelloWorld = SET "hello" "world"

addLanguageToFavorites : String → RedisPrimitiveCommand ⊤
addLanguageToFavorites = PREPEND "favoriteLanguages"

{-
   Ok! Now let's define our abstractions. I like to think of relations
   between data types as paths, so for example, in a social network we
   would have a path from UserId to Profile, a path from PostId to Post, etc.

   Note that as in a category, there may be multiple paths between two types! For
   example, `userPosts` and `userReposts` would be two distinct paths from
   UserId to List PostId.

   To distinguish between paths, I'll simply name them with a String.
-}

record Path (a b : Set) {{_ : Serializable a}} {{_ : Serializable b}} : Set where
  constructor name
  field
    prefix : String

record ListPath (a b : Set) {{_ : Serializable a}} {{_ : Serializable b}} : Set where
  constructor name
  field
    prefix : String

{-
   We'll get back to using these Path types in a minute. For now, we need a
   way to represent sequences of Redis commands as a data structure. Rather than
   deal with the sequencing manually, we can simply defer this to the Free monad,
   meaning all we really need from our Command structure is a Functor.

   Simply providing a decoder parameter for each constructor will give us enough
   power to make a Functor.
-}

private
  data Command {ℓ} : Set ℓ → Set ℓ where
    lookup : ∀ {t : Set ℓ} → (key : String) → (Maybe String → t) → Command t
    lookupList : ∀ {t : Set ℓ} → (key : String) → (List String → t) → Command t
    store : ∀ {t} (key value : String) → (⊤ → t) → Command t
    prepend : ∀ {t} (key value : String) → (⊤ → t) → Command t
    delete : ∀ {t} (key : String) → (⊤ → t) → Command t

  mapOp : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} → (t₁ → t₂) → Command t₁ → Command t₂
  mapOp f (lookup x d) = lookup x (f ∘ d)
  mapOp f (lookupList x d) = lookupList x (f ∘ d)
  mapOp f (store key value x) = store key value (λ _ → f (x tt))
  mapOp f (prepend key value x) = prepend key value (λ _ → f (x tt))
  mapOp f (delete key x) = delete key (λ _ → f (x tt))

  instance
    commandIsFunctor : ∀ {ℓ₁ ℓ₂} → Functor Command ℓ₁ ℓ₂
    commandIsFunctor = record { _<$>_ = mapOp }

  Redis = Free Command

{-
   To use our new Redis monad, we need to reify it back into IO. As an aside,
   it's possible to define a pure implementation of Redis's primitives and
   reify into that as well, meaning you could state and prove mathematical
   properties about your relations and queries.

   But for this article, we'll just reify back to IO.
-}

{-# TERMINATING #-}
reifyToPrimitive : ∀ {ℓ} {t : Set ℓ} → Redis t → RedisPrimitiveCommand t
reifyToPrimitive (Pure x) = pure x
reifyToPrimitive (MkFree (lookup x d)) = d <$> GET x >>= reifyToPrimitive
reifyToPrimitive (MkFree (lookupList x d)) = d <$> GETLIST x >>= reifyToPrimitive
reifyToPrimitive (MkFree (store key value d)) = d <$> SET key value >>= reifyToPrimitive
reifyToPrimitive (MkFree (prepend key value d)) = d <$> PREPEND key value >>= reifyToPrimitive
reifyToPrimitive (MkFree (delete key d)) = d <$> DELETE key >>= reifyToPrimitive

{-
   And one final piece to complete our abstraction: connect our Path concept to our new
   Redis monad! Since the implementation of Command is private, access via a Path as
   defined below is the only way to create a `Redis t`.
-}

open Serializable {{...}}

lookupPath : ∀ {a b} {{_ : Serializable a}} {{_ : Serializable b}} → Path a b → a → Redis (Maybe b)
lookupPath (name prefix) x = wrap (lookup (prefix ++ serialize x) (λ x → join (deserialize <$> x)))

lookupListPath : ∀ {a b} {{_ : Serializable a}} {{_ : Serializable b}} → ListPath a b → a → Redis (List b)
lookupListPath (name prefix) x = wrap (lookupList (prefix ++ serialize x) (λ x → filter id (deserialize <$> x)))

setPath : ∀ {a b} {{_ : Serializable a}} {{_ : Serializable b}} → Path a b → a → b → Redis ⊤
setPath (name prefix) k v = wrap (store (prefix ++ serialize k) (serialize v) id)

prependPath : ∀ {a b} {{_ : Serializable a}} {{_ : Serializable b}} → ListPath a b → a → b → Redis ⊤
prependPath (name prefix) k v = wrap (prepend (prefix ++ serialize k) (serialize v) id)

deletePath : ∀ {a b} {{_ : Serializable a}} {{_ : Serializable b}} → Path a b → a → Redis ⊤
deletePath (name prefix) k = wrap (delete (prefix ++ serialize k) id)


runRedis : ∀ {ℓ} {t : Set ℓ} → Redis t → IO t
runRedis = reifyToPrimitive

{-
   And we're done! We can now define paths between our application data
   types and control them via the Redis monad. Below are some usage examples
   demonstrating how concise and safe our API is:
-}

-- postulate some typical application types and their serializability

postulate
  UserId PostId Profile Post : Set

  instance
    userIdIsSerializable : Serializable UserId
    postIdIsSerializable : Serializable PostId
    profileIsSerializable : Serializable Profile
    postIsSerializable : Serializable Post

-- and declare some Paths between our data types

UserId:Profile : Path UserId Profile
UserId:Profile = name "userIdToProfile"

UserId:Friends : ListPath UserId UserId
UserId:Friends = name "userIdToFriends"

UserId:Posts : ListPath UserId PostId
UserId:Posts = name "userIdToPosts"

PostId:Post : Path PostId Post
PostId:Post = name "postIdToPost"

-- and make our core application API!

getUserProfile : UserId → Redis (Maybe Profile)
getUserProfile = lookupPath UserId:Profile

getPost : PostId → Redis (Maybe Post)
getPost = lookupPath PostId:Post

getUserFriends : UserId → Redis (List Profile)
getUserFriends = lookupListPath UserId:Friends >=> filterA getUserProfile

getUserPosts : UserId → Redis (List Post)
getUserPosts = lookupListPath UserId:Posts >=> filterA getPost

createPost : UserId → PostId → Post → Redis ⊤
createPost userId postId post =
  setPath PostId:Post postId post >>= λ _ →
  prependPath UserId:Posts userId postId