Copyright	© 2021-2023 IOHK 2024 Cardano Foundation
License	Apache-2.0
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Delta.Embedding

Contents

Internal

Description

Embeddings of delta types.

Synopsis

data Embedding da db
data Embedding' da db where
- Embedding' :: (Delta da, Delta db, a ~ Base da, b ~ Base db) => {..} -> Embedding' da db
mkEmbedding :: Embedding' da db -> Embedding da db
fromEmbedding :: (Delta da, Delta db) => Embedding da db -> Embedding' da db
pair :: Embedding da1 db1 -> Embedding da2 db2 -> Embedding (da1, da2) (db1, db2)
liftUpdates :: Delta da => Embedding da db -> [da] -> Base da -> (Base db, [db])
replaceFromApply :: (Delta da, a ~ Base da) => Embedding' da (Replace a)
inject :: Embedding da db -> Base da -> Machine da db
project :: Embedding da db -> Base db -> Either SomeException (Base da, Machine da db)

Documentation

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
```
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
```
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

apply (update a (write a) da) (write a) ≠ write (apply da a)

data Embedding da db Source #

Embedding with efficient composition o. To construct an embedding, use mkEmbedding.

Instances

Instances details

Semigroupoid Embedding Source #	Efficient composition of `Embedding`
Instance details Defined in Data.Delta.Embedding Methods o :: forall (j :: k) (k1 :: k) (i :: k). Embedding j k1 -> Embedding i j -> Embedding i k1 #

data Embedding' da db where Source #

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 for a more detailed description.

Constructors

Embedding'
Fields :: (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

mkEmbedding :: Embedding' da db -> Embedding da db Source #

Construct Embedding with efficient composition

fromEmbedding :: (Delta da, Delta db) => Embedding da db -> Embedding' da db Source #

Extract load, write, and update functions from an efficient Embedding.

pair :: Embedding da1 db1 -> Embedding da2 db2 -> Embedding (da1, da2) (db1, db2) Source #

A pair of Embeddings gives an embedding of pairs.

liftUpdates Source #

Arguments

:: 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)).

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)

replaceFromApply :: (Delta da, a ~ Base da) => Embedding' da (Replace a) Source #

Having an apply function is equivalent to the existence of a canonical embedding into the trivial Replace delta type.

Internal

inject :: Embedding da db -> Base da -> Machine da db Source #

project :: Embedding da db -> Base db -> Either SomeException (Base da, Machine da db) Source #