Embedding.hs

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-|
Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation
License: Apache-2.0

Embeddings of delta types.
-}
module Data.Delta.Embedding (
    -- $Embedding
      Embedding
    , Embedding' (..)
    , mkEmbedding
    , fromEmbedding
    , pair
    , liftUpdates
    , replaceFromApply

    -- * Internal
    , inject
    , project
    ) where

import Prelude

import Control.Exception
    ( SomeException
    )
import Data.Delta.Core
    ( Delta (..)
    , Replace (..)
    )
import Data.Delta.Embedding.Internal
    ( Machine (..)
    , fromState
    , pairMachine
    )
import Data.Either
    ( fromRight
    )
import Data.Semigroupoid
    ( Semigroupoid (..)
    )

{-------------------------------------------------------------------------------
    Embedding
-------------------------------------------------------------------------------}
{- $Embedding
#doc:Embedding#

An 'Embedding'@ da db@ embeds one type and its delta type @da@
into another type and its delta type @db@.

For reasons of efficiency, 'Embedding' is an abstract type.
It is constructed using the 'Embedding'' type, which has
three components.

* 'write' embeds values from the type @a = 'Base' da@
    into the type @b = 'Base' db@.
* 'load' attempts to retrieve the value of type @a@
    from the type @b@, but does not necessarily succeed.
* 'update' maps a delta type @da@ to a delta type @db@.
    For this mapping, both the value of type @a@ and a corresponding
    value of type @b@ are provided;
    the delta types @da@ and @db@ are relative to these values.
    In the definition of 'update', we can assume that @Right a = load b@.

The embedding of one type into the other is characterized by the following
properties:

* The embedding is __not necessarily surjective__:
    The type @b@ may contain many values that do not correspond to
    a value of type @a@. Hence, 'load' has an 'Either' result.
    (See Note [EitherSomeException] for the choice of exception type.)
    However, retrieving a written value always succeeds, we have

        prop> load . write = Right

* The embedding is __redundant__:
    The type @b@ may contain multiple values that correspond to
    one and the same @a@.
    This is why the 'update' function expects the type @b@ as argument,
    so that the right deltas can be computed.
    Put differently, we often have

        prop> write a ≠ b   where Right a = load b

* The embedding of a delta __commutes with 'apply'__.
    We have

        > Right (apply da a) = load (apply (update a b da) b)
        >     where Right a = load b

    However, since the embedding is redundant, we often have

        prop> apply (update a (write a) da) (write a) ≠ write (apply da a)
-}

-- | Specification of an embedding of a type @a@ with delta types @da@
-- into the type @b@ with delta type @db@.
-- See [the discussion of @Embedding@](#doc:Embedding)
-- for a more detailed description.
data Embedding' da db where
    Embedding'
        :: (Delta da, Delta db, a ~ Base da, b ~ Base db) =>
        { load   :: b -> Either SomeException a
        , write  :: a -> b
        , update :: a -> b -> da -> db
        } -> Embedding' da db

-- | 'Embedding' with efficient composition 'o'.
-- To construct an embedding, use 'mkEmbedding'.
data Embedding da db = Embedding
    { inject  :: Base da -> Machine da db
    , project :: Base db -> Either SomeException (Base da, Machine da db)
    }

-- | Construct 'Embedding' with efficient composition
mkEmbedding :: Embedding' da db -> Embedding da db
mkEmbedding Embedding'{load,write,update} = Embedding
    { inject = start . write
    , project = \b -> (, start b) <$> load b
    }
  where
    start b = fromState step (b,())
    step (a,da) (b,_) = (update a b da, ())

-- | Extract 'load', 'write', and 'update' functions
-- from an efficient 'Embedding'.
fromEmbedding :: (Delta da, Delta db) => Embedding da db -> Embedding' da db
fromEmbedding Embedding{inject,project} = Embedding'
    { load = fmap fst . project
    , write = state_ . inject
    , update = \a b da ->
        let (_ ,mab) = from (project b)
            (db,_  ) = step_ mab (a,da)
        in  db
    }
  where
    from = fromRight (error "Embedding: 'load' violates expected laws")

-- | Efficient composition of 'Embedding'
instance Semigroupoid Embedding where
    (Embedding inject2 project2) `o` (Embedding inject1 project1) =
        Embedding{inject,project}
      where
        inject a =
            let mab = inject1 a
                mbc = inject2 (state_ mab)
            in  mbc `o` mab
        project c = do
            (b, mbc) <- project2 c
            (a, mab) <- project1 b
            pure (a, mbc `o` mab)

-- | A pair of 'Embedding's gives an embedding of pairs.
pair :: Embedding da1 db1 -> Embedding da2 db2 -> Embedding (da1,da2) (db1,db2)
pair (Embedding inject1 project1) (Embedding inject2 project2) =
    Embedding{inject,project}
  where
    inject (a1,a2) = pairMachine (inject1 a1) (inject2 a2)
    project (b1,b2) = do
        (a1, m1) <- project1 b1
        (a2, m2) <- project2 b2
        pure ((a1,a2), pairMachine m1 m2)

-- | Lift a sequence of updates through an 'Embedding'.
--
-- >   (b, dbs) = liftUpdates (mkEmbedding embedding') das a
-- > implies
-- >   load embedding' b = Right (apply das a)
-- >   b = apply dbs (write embedding' a)
liftUpdates
    :: Delta da
    => Embedding da db
    -> [da]
    -- ^ List of deltas to apply.
    -- The deltas are applied right-to-left; the 'head' is applied __last__.
    -> Base da
    -- ^ Base value to apply the deltas to.
    -> (Base db, [db])
    -- ^ (Final base value, updates that were applied ('head' is __last__)).
liftUpdates Embedding{inject} das0 a0 =
    let (b,dbs) = go (inject a0) a0 (reverse das0) in (b, reverse dbs)
  where
    go machine1 _  [] = (state_ machine1, [])
    go machine1 !a (da:das) = (b,db:dbs)
      where
        (b ,dbs) = go machine2 (apply da a) das
        (db,machine2) = step_ machine1 (a,da)

-- | Having an 'apply' function is equivalent to the existence
-- of a canonical embedding into the trivial 'Replace' delta type.
replaceFromApply :: (Delta da, a ~ Base da) => Embedding' da (Replace a)
replaceFromApply = Embedding'
    { load = Right
    , write = id
    , update = \_ a da -> Replace (apply da a)
    }

{-
-- | Use the 'update' function of an 'Embedding' to convert
-- one delta type to another.
--
-- This function assumes that the 'Embedding' argument satisfies
-- @load = Just@ and @write = id@.
applyWithEmbedding
    :: (Delta db, a ~ Base db)
    => Embedding da db -> (da -> a -> a)
applyWithEmbedding e delta1 a = apply (update e a delta1) a
-}