delta-types (empty) → 1.0.0.0
raw patch · 16 files changed
+1436/−0 lines, 16 filesdep +QuickCheckdep +basedep +containers
Dependencies added: QuickCheck, base, containers, delta-types, hspec, semigroupoids
Files
- CHANGELOG.md +5/−0
- LICENSE +202/−0
- README.md +32/−0
- delta-types.cabal +97/−0
- src/Data/Delta.hs +48/−0
- src/Data/Delta/Core.hs +123/−0
- src/Data/Delta/Embedding.hs +216/−0
- src/Data/Delta/Embedding/Internal.hs +71/−0
- src/Data/Delta/List.hs +42/−0
- src/Data/Delta/Map.hs +41/−0
- src/Data/Delta/Set.hs +118/−0
- test/unit/Data/Delta/CoreSpec.hs +55/−0
- test/unit/Data/Delta/EmbeddingSpec.hs +209/−0
- test/unit/Data/Delta/ListSpec.hs +55/−0
- test/unit/Data/Delta/SetSpec.hs +121/−0
- test/unit/Main.hs +1/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for delta-types++## 1.0.0.0 — 2025-02-26++* Initial version
+ LICENSE view
@@ -0,0 +1,202 @@++ Apache License+ Version 2.0, January 2004+ http://www.apache.org/licenses/++ TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION++ 1. Definitions.++ "License" shall mean the terms and conditions for use, reproduction,+ and distribution as defined by Sections 1 through 9 of this document.++ "Licensor" shall mean the copyright owner or entity authorized by+ the copyright owner that is granting the License.++ "Legal Entity" shall mean the union of the acting entity and all+ other entities that control, are controlled by, or are under common+ control with that entity. For the purposes of this definition,+ "control" means (i) the power, direct or indirect, to cause the+ direction or management of such entity, whether by contract or+ otherwise, or (ii) ownership of fifty percent (50%) or more of the+ outstanding shares, or (iii) beneficial ownership of such entity.++ "You" (or "Your") shall mean an individual or Legal Entity+ exercising permissions granted by this License.++ "Source" form shall mean the preferred form for making modifications,+ including but not limited to software source code, documentation+ source, and configuration files.++ "Object" form shall mean any form resulting from mechanical+ transformation or translation of a Source form, including but+ not limited to compiled object code, generated documentation,+ and conversions to other media types.++ "Work" shall mean the work of authorship, whether in Source or+ Object form, made available under the License, as indicated by a+ copyright notice that is included in or attached to the work+ (an example is provided in the Appendix below).++ "Derivative Works" shall mean any work, whether in Source or Object+ form, that is based on (or derived from) the Work and for which the+ editorial revisions, annotations, elaborations, or other modifications+ represent, as a whole, an original work of authorship. For the purposes+ of this License, Derivative Works shall not include works that remain+ separable from, or merely link (or bind by name) to the interfaces of,+ the Work and Derivative Works thereof.++ "Contribution" shall mean any work of authorship, including+ the original version of the Work and any modifications or additions+ to that Work or Derivative Works thereof, that is intentionally+ submitted to Licensor for inclusion in the Work by the copyright owner+ or by an individual or Legal Entity authorized to submit on behalf of+ the copyright owner. For the purposes of this definition, "submitted"+ means any form of electronic, verbal, or written communication sent+ to the Licensor or its representatives, including but not limited to+ communication on electronic mailing lists, source code control systems,+ and issue tracking systems that are managed by, or on behalf of, the+ Licensor for the purpose of discussing and improving the Work, but+ excluding communication that is conspicuously marked or otherwise+ designated in writing by the copyright owner as "Not a Contribution."++ "Contributor" shall mean Licensor and any individual or Legal Entity+ on behalf of whom a Contribution has been received by Licensor and+ subsequently incorporated within the Work.++ 2. Grant of Copyright License. Subject to the terms and conditions of+ this License, each Contributor hereby grants to You a perpetual,+ worldwide, non-exclusive, no-charge, royalty-free, irrevocable+ copyright license to reproduce, prepare Derivative Works of,+ publicly display, publicly perform, sublicense, and distribute the+ Work and such Derivative Works in Source or Object form.++ 3. Grant of Patent License. Subject to the terms and conditions of+ this License, each Contributor hereby grants to You a perpetual,+ worldwide, non-exclusive, no-charge, royalty-free, irrevocable+ (except as stated in this section) patent license to make, have made,+ use, offer to sell, sell, import, and otherwise transfer the Work,+ where such license applies only to those patent claims licensable+ by such Contributor that are necessarily infringed by their+ Contribution(s) alone or by combination of their Contribution(s)+ with the Work to which such Contribution(s) was submitted. If You+ institute patent litigation against any entity (including a+ cross-claim or counterclaim in a lawsuit) alleging that the Work+ or a Contribution incorporated within the Work constitutes direct+ or contributory patent infringement, then any patent licenses+ granted to You under this License for that Work shall terminate+ as of the date such litigation is filed.++ 4. Redistribution. You may reproduce and distribute copies of the+ Work or Derivative Works thereof in any medium, with or without+ modifications, and in Source or Object form, provided that You+ meet the following conditions:++ (a) You must give any other recipients of the Work or+ Derivative Works a copy of this License; and++ (b) You must cause any modified files to carry prominent notices+ stating that You changed the files; and++ (c) You must retain, in the Source form of any Derivative Works+ that You distribute, all copyright, patent, trademark, and+ attribution notices from the Source form of the Work,+ excluding those notices that do not pertain to any part of+ the Derivative Works; and++ (d) If the Work includes a "NOTICE" text file as part of its+ distribution, then any Derivative Works that You distribute must+ include a readable copy of the attribution notices contained+ within such NOTICE file, excluding those notices that do not+ pertain to any part of the Derivative Works, in at least one+ of the following places: within a NOTICE text file distributed+ as part of the Derivative Works; within the Source form or+ documentation, if provided along with the Derivative Works; or,+ within a display generated by the Derivative Works, if and+ wherever such third-party notices normally appear. The contents+ of the NOTICE file are for informational purposes only and+ do not modify the License. You may add Your own attribution+ notices within Derivative Works that You distribute, alongside+ or as an addendum to the NOTICE text from the Work, provided+ that such additional attribution notices cannot be construed+ as modifying the License.++ You may add Your own copyright statement to Your modifications and+ may provide additional or different license terms and conditions+ for use, reproduction, or distribution of Your modifications, or+ for any such Derivative Works as a whole, provided Your use,+ reproduction, and distribution of the Work otherwise complies with+ the conditions stated in this License.++ 5. Submission of Contributions. Unless You explicitly state otherwise,+ any Contribution intentionally submitted for inclusion in the Work+ by You to the Licensor shall be under the terms and conditions of+ this License, without any additional terms or conditions.+ Notwithstanding the above, nothing herein shall supersede or modify+ the terms of any separate license agreement you may have executed+ with Licensor regarding such Contributions.++ 6. Trademarks. This License does not grant permission to use the trade+ names, trademarks, service marks, or product names of the Licensor,+ except as required for reasonable and customary use in describing the+ origin of the Work and reproducing the content of the NOTICE file.++ 7. Disclaimer of Warranty. Unless required by applicable law or+ agreed to in writing, Licensor provides the Work (and each+ Contributor provides its Contributions) on an "AS IS" BASIS,+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+ implied, including, without limitation, any warranties or conditions+ of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A+ PARTICULAR PURPOSE. You are solely responsible for determining the+ appropriateness of using or redistributing the Work and assume any+ risks associated with Your exercise of permissions under this License.++ 8. Limitation of Liability. In no event and under no legal theory,+ whether in tort (including negligence), contract, or otherwise,+ unless required by applicable law (such as deliberate and grossly+ negligent acts) or agreed to in writing, shall any Contributor be+ liable to You for damages, including any direct, indirect, special,+ incidental, or consequential damages of any character arising as a+ result of this License or out of the use or inability to use the+ Work (including but not limited to damages for loss of goodwill,+ work stoppage, computer failure or malfunction, or any and all+ other commercial damages or losses), even if such Contributor+ has been advised of the possibility of such damages.++ 9. Accepting Warranty or Additional Liability. While redistributing+ the Work or Derivative Works thereof, You may choose to offer,+ and charge a fee for, acceptance of support, warranty, indemnity,+ or other liability obligations and/or rights consistent with this+ License. However, in accepting such obligations, You may act only+ on Your own behalf and on Your sole responsibility, not on behalf+ of any other Contributor, and only if You agree to indemnify,+ defend, and hold each Contributor harmless for any liability+ incurred by, or claims asserted against, such Contributor by reason+ of your accepting any such warranty or additional liability.++ END OF TERMS AND CONDITIONS++ APPENDIX: How to apply the Apache License to your work.++ To apply the Apache License to your work, attach the following+ boilerplate notice, with the fields enclosed by brackets "[]"+ replaced with your own identifying information. (Don't include+ the brackets!) The text should be enclosed in the appropriate+ comment syntax for the file format. We also recommend that a+ file or class name and description of purpose be included on the+ same "printed page" as the copyright notice for easier+ identification within third-party archives.++ Copyright [yyyy] [name of copyright owner]++ Licensed under the Apache License, Version 2.0 (the "License");+ you may not use this file except in compliance with the License.+ You may obtain a copy of the License at++ http://www.apache.org/licenses/LICENSE-2.0++ Unless required by applicable law or agreed to in writing, software+ distributed under the License is distributed on an "AS IS" BASIS,+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+ See the License for the specific language governing permissions and+ limitations under the License.
+ README.md view
@@ -0,0 +1,32 @@+## Overview++This package provides a notion of *delta types* via the `Delta` typeclass.++A *delta type* `da` for a *base type* `a` is a collection of values that each correspond to a change `a → a` of the base type. The following typeclass captures this correspondence:++ class Delta da where+ type Base da = a+ apply :: da → (a → a)++In the literature, this concept is also known as a *change action*, with relations to incremental computation and differential lambda calculus. See References.++For example, one delta type for `Set a` is given by++ data DeltaSet1 a = Insert a | Delete a+ + instance Delta (DeltaSet1 a) where+ type Base (DeltaSet1 a) = Set a+ apply (Insert a) = Data.Set.insert a+ apply (Delete a) = Date.Set.delete a++In general, there may be multiple delta types associated with a single base type.++## References++1. Alvarez-Picallo, M., Eyers-Taylor, A., Peyton Jones, M., Ong, CH.L. (2019). [Fixing Incremental Computation][1811.06069]. In: Caires, L. (eds) Programming Languages and Systems. ESOP 2019. Lecture Notes in Computer Science(), vol 11423. Springer, Cham.+2. M. Alvarez-Picallo, M. (2020). [Change actions: from incremental computation to discrete derivatives][2002.05256]. PhD thesis, Oxford.+3. Apfelmus, H. (2023). [Delta encodings help separate business logic from database operations][bobkonf2023]. Bobkonf 2023, Berlin.++ [bobkonf2023]: https://bobkonf.de/2023/apfelmus.html+ [2002.05256]: https://arxiv.org/abs/2002.05256+ [1811.06069]: https://arxiv.org/abs/1811.06069
+ delta-types.cabal view
@@ -0,0 +1,97 @@+cabal-version: 2.2+name: delta-types+version: 1.0.0.0+synopsis: Delta types, also known as change actions.+description:+ A __delta type__ @da@ for a __base type__ @a@ is a collection+ of values, each of which corresponds to a change @a → a@ of the base type.+ .+ See also+ .+ * [Delta encodings help separate business logic from database operations](https://bobkonf.de/2023/apfelmus.html)+ .+ * [Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog](http://arxiv.org/abs/1811.06069)+ (Here, the concept of a delta type is called a __change action__.)++homepage: https://github.com/cardano-foundation/delta-types+license: Apache-2.0+license-file: LICENSE+author: Cardano Foundation (High Assurance Lab)+maintainer: hal@cardanofoundation.org+copyright: 2021-2023 IOHK, 2024-2025 Cardano Foundation+category: Data Structures+build-type: Simple+tested-with: GHC ==8.10.7 || ==9.6.6 || ==9.10.1+extra-doc-files:+ CHANGELOG.md+ README.md++common language+ default-language: Haskell2010+ default-extensions:+ NoImplicitPrelude+ OverloadedStrings++ other-extensions:+ BangPatterns+ FlexibleContexts+ GADTs+ NamedFieldPuns+ StandaloneDeriving+ TupleSections+ TypeFamilies+ TypeOperators+ UndecidableInstances++common opts-lib+ ghc-options:+ -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns+ -Wincomplete-record-updates++ if flag(release)+ ghc-options: -O2 -Werror++common opts-exe+ import: opts-lib+ ghc-options: -threaded -rtsopts++flag release+ description: Enable optimization and `-Werror`+ default: False+ manual: True++library+ import: language, opts-lib+ hs-source-dirs: src+ build-depends:+ , base >=4.14 && <5+ , containers >=0.5 && <0.9+ , semigroupoids >=6.0.1 && <6.1++ exposed-modules:+ Data.Delta+ Data.Delta.Core+ Data.Delta.Embedding+ Data.Delta.Embedding.Internal+ Data.Delta.List+ Data.Delta.Map+ Data.Delta.Set++test-suite unit+ import: language, opts-exe+ type: exitcode-stdio-1.0+ hs-source-dirs: test/unit+ main-is: Main.hs+ build-depends:+ , base+ , containers+ , delta-types+ , hspec >=2.11.0 && <2.12+ , QuickCheck >=2.14 && <2.16++ build-tool-depends: hspec-discover:hspec-discover+ other-modules:+ Data.Delta.CoreSpec+ Data.Delta.EmbeddingSpec+ Data.Delta.ListSpec+ Data.Delta.SetSpec
+ src/Data/Delta.hs view
@@ -0,0 +1,48 @@+{-|+Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation+License: Apache-2.0++Delta types are instances of the type class 'Delta'.+An instance 'Delta'@ delta@ indicates that the type @delta@+is a delta type of the corresponding base type 'Base'@ delta@.+The 'apply' function applies a delta to the base type.++Delta types can be transformed into each other using the 'Embedding' type.+'Embedding's can be composed using the 'Semigroupoid' class.++Examples:++prop> apply (Replace 7) 3 = 7+prop> apply [Append [1], Append [2]] [3] = [1,2,3]+prop> apply [Insert 'c', Delete 'b'] (Set.fromList "ab") = Set.fromList "ac"+prop> ∀(x :: Set Char). apply [Delete 'b', Insert 'b'] x = apply (Delete 'b') x+-}+module Data.Delta (+ -- * Modules++ -- | The present module re-exports the following child modules+ -- for convenience.+ --+ -- Core definitions:+ -- 'Delta' class, 'apply' function, 'Base' type family.+ --+ -- Core instances:+ -- 'Replace', 'Data.Monoid.Endo', 'Data.Maybe.Maybe', '[]'.+ module Data.Delta.Core++ -- | Delta types for common containers.+ , module Data.Delta.List+ , module Data.Delta.Set++ -- | Embeddings of delta types and helper functions.+ , module Data.Delta.Embedding++ -- | Re-export "Data.Semigroupoid" for convenience.+ , module Data.Semigroupoid+ ) where++import Data.Delta.Core+import Data.Delta.Embedding+import Data.Delta.List+import Data.Delta.Set+import Data.Semigroupoid
+ src/Data/Delta/Core.hs view
@@ -0,0 +1,123 @@+{-# LANGUAGE TypeFamilies #-}++{-|+Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation+License: Apache-2.0+-}+module Data.Delta.Core+ ( Delta (..)+ , NoChange (..)+ , Replace (..)+ ) where++import Prelude++import Data.Kind+ ( Type+ )+import Data.List.NonEmpty+ ( NonEmpty+ )+import Data.Monoid+ ( Endo (..)+ )++{-------------------------------------------------------------------------------+ Delta types+-------------------------------------------------------------------------------}+-- | Type class for delta types.+class Delta delta where+ -- | Base type for which @delta@ represents a delta.+ -- This is implemented as a type family, so that we can have+ -- multiple delta types for the same base type.+ type Base delta :: Type+ -- | Apply a delta to the base type.+ --+ -- Whenever the type @delta@ is a 'Semigroup', we require that+ --+ -- prop> apply (d1 <> d2) = apply d1 . apply d2+ --+ -- This means that deltas are applied __right-to-left__:+ -- @d1@ is applied __after__ @d2@.+ --+ -- Whenever the type @delta@ is a 'Monoid', we require that+ --+ -- prop> apply mempty = id+ apply :: delta -> Base delta -> Base delta++-- | 'Endo' is the most general delta, which allows any change.+instance Delta (Endo a) where+ type Base (Endo a) = a+ apply (Endo f) = f++-- | The least general delta, where nothing is changed.+data NoChange (a :: Type) = NoChange+ deriving (Eq, Ord, Show)++-- | prop> apply NoChange a = a+instance Delta (NoChange a) where+ type Base (NoChange a) = a+ apply _ a = a++-- | Trivial delta type for the type @a@ that replaces the value wholesale.+newtype Replace a = Replace a+ deriving (Eq, Ord, Show)++-- |+-- prop> apply (Replace a) _ = a+instance Delta (Replace a) where+ type Base (Replace a) = a+ apply (Replace a) _ = a++-- | Combine replacements. The first argument takes precedence.+-- Hence, 'apply' is a morphism:+--+-- prop> apply (Replace a <> Replace b) = apply (Replace a) . apply (Replace b)+--+-- More strongly, we have+--+-- prop> apply (Replace a <> _) = apply (Replace a)+instance Semigroup (Replace a) where+ r <> _ = r++-- | A delta can be optionally applied.+instance Delta delta => Delta (Maybe delta) where+ type Base (Maybe delta) = Base delta+ apply = maybe id apply++-- | A list of deltas can be applied like a single delta.+-- This overloading of 'apply' is very convenient.+--+-- Order is important: The 'head' of the list is applied __last__,+-- so deltas are applied __right-to-left__.+-- Hence, 'apply' is a morphism+--+-- prop> apply [] = id+-- prop> apply (d1 ++ d2) = apply d1 . apply d2+instance Delta delta => Delta [delta] where+ type Base [delta] = Base delta+ apply ds a = foldr apply a ds++-- | For convenience, a nonempty list of deltas+-- can be applied like a list of deltas.+--+-- Remember that deltas are applied right-to-left.+instance Delta delta => Delta (NonEmpty delta) where+ type Base (NonEmpty delta) = Base delta+ apply ds a = foldr apply a ds++-- | A pair of deltas represents a delta for a pair.+instance (Delta d1, Delta d2) => Delta (d1,d2) where+ type Base (d1, d2) = (Base d1, Base d2)+ apply (d1,d2) (a1,a2) = (apply d1 a1, apply d2 a2)++-- | A triple of deltas represents a delta for a triple.+instance (Delta d1, Delta d2, Delta d3) => Delta (d1,d2,d3) where+ type Base (d1,d2,d3) = (Base d1,Base d2,Base d3)+ apply (d1,d2,d3) (a1,a2,a3) = (apply d1 a1, apply d2 a2, apply d3 a3)++-- | A 4-tuple of deltas represents a delta for a 4-tuple.+instance (Delta d1, Delta d2, Delta d3, Delta d4) => Delta (d1,d2,d3,d4) where+ type Base (d1,d2,d3,d4) = (Base d1,Base d2,Base d3,Base d4)+ apply (d1,d2,d3,d4) (a1,a2,a3,a4) =+ (apply d1 a1, apply d2 a2, apply d3 a3, apply d4 a4)
+ src/Data/Delta/Embedding.hs view
@@ -0,0 +1,216 @@+{-# 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+-}
+ src/Data/Delta/Embedding/Internal.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Copyright: © 2021-2023 IOHK, 2024-2025 Cardano Foundation+License: Apache-2.0++Internal representation of 'Embedding'+in terms of state machines.+-}+module Data.Delta.Embedding.Internal (+ Machine (..)+ , idle+ , pairMachine+ , fromState+ ) where++import Prelude++import Data.Delta.Core+ ( Delta (..)+ )+import Data.Semigroupoid+ ( Semigroupoid (..)+ )++{-------------------------------------------------------------------------------+ Machine (state machines) with efficient composition+-------------------------------------------------------------------------------}+-- Strict pair.+-- If a value of this type is in WHNF, so are the two components.+-- data StrictPair a b = !a :*: !b+-- infixr 1 :*:++-- | A state machine that maps deltas to deltas.+-- This machine always carries a state of type 'Base'@ db@ around.+data Machine da db = Machine+ { state_ :: !(Base db)+ , step_ :: (Base da, da) -> (db, Machine da db)+ }++-- | Composition of 'Machine'+instance Semigroupoid Machine where+ (Machine c fbc) `o` (Machine b fab) = Machine c $ \ada ->+ case fab ada of+ (db, mab) -> case fbc (b,db) of+ (dc, mbc) -> (dc, mbc `o` mab)++-- | Identity machine starting from a base type.+idle :: Delta da => Base da -> Machine da da+idle a0 = Machine a0 $ \(a1,da) -> let a2 = apply da a1 in (da, idle a2)++-- | Pair two 'Machine's.+pairMachine+ :: Machine da1 db1 -> Machine da2 db2 -> Machine (da1,da2) (db1,db2)+pairMachine (Machine s1 step1) (Machine s2 step2) =+ Machine (s1,s2) $ \((a1,a2), (da1,da2)) ->+ let (db1, m1) = step1 (a1,da1)+ (db2, m2) = step2 (a2,da2)+ in ((db1,db2), pairMachine m1 m2)++-- | Create a 'Machine' from a specific state @s@,+-- and the built-in state 'Base'@ db@.+fromState+ :: Delta db+ => ((Base da, da) -> (Base db, s) -> (db, s))+ -> (Base db, s)+ -> Machine da db+fromState step (b,s0) = Machine b $ \ada ->+ case step ada (b,s0) of+ (db,s1) -> (db, fromState step (apply db b,s1))
+ src/Data/Delta/List.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE TypeFamilies #-}++{-|+Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation+License: Apache-2.0++Delta types for lists.+-}+module Data.Delta.List+ ( DeltaList (..)+ ) where++import Prelude++import Data.Delta.Core+ ( Delta (..)+ )++{-------------------------------------------------------------------------------+ Delta type for lists+-------------------------------------------------------------------------------}++-- | Delta type for lists where a list of elements is prepended.+newtype DeltaList a = Append [a]+ deriving (Eq, Ord, Show)++-- |+-- prop> apply (Append xs) ys = xs ++ ys+instance Delta (DeltaList a) where+ type Base (DeltaList a) = [a]+ apply (Append xs) ys = xs ++ ys++-- | Remember that the semigroup instance is required to satisfy+-- the following properties:+--+-- prop> apply mempty = id+-- prop> apply (d1 <> d2) = apply d1 . apply d2+instance Ord a => Semigroup (DeltaList a) where+ (Append xs) <> (Append ys) = Append (xs ++ ys)++instance Ord a => Monoid (DeltaList a) where+ mempty = Append []
+ src/Data/Delta/Map.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++{-|+Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation+License: Apache-2.0++Delta types for 'Data.Map.Map'.+-}+module Data.Delta.Map+ ( DeltaMap(..)+ ) where++import Prelude++import Data.Delta.Core+ ( Delta (..)+ )+import Data.Map.Strict+ ( Map+ )+import qualified Data.Map.Strict as Map++{-------------------------------------------------------------------------------+ Delta type for 'Map'+-------------------------------------------------------------------------------}+-- | Delta type for 'Map'.+data DeltaMap key da+ = Insert key (Base da)+ | Delete key+ | Adjust key da++deriving instance (Show key, Show da, Show (Base da)) => Show (DeltaMap key da)+instance (Ord key, Delta da)+ => Delta (DeltaMap key da) where+ type Base (DeltaMap key da) = Map key (Base da)+ apply (Insert key a) = Map.insert key a+ apply (Delete key) = Map.delete key+ apply (Adjust key da) = Map.adjust (apply da) key
+ src/Data/Delta/Set.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation+License: Apache-2.0++Delta types for 'Set'.+-}+module Data.Delta.Set+ ( -- * Single element+ DeltaSet1 (..)+ -- $DeltaSet1-laws++ -- * Multiple elements+ , DeltaSet+ , diffSet+ , listFromDeltaSet+ , deltaSetFromList+ ) where++import Prelude++import Data.Delta.Core+ ( Delta (..)+ )+import Data.Set+ ( Set+ )++import qualified Data.Set as Set++{-------------------------------------------------------------------------------+ DeltaSet+-------------------------------------------------------------------------------}++-- | Delta type for 'Set' where a single element is deleted or added.+data DeltaSet1 a+ = Insert a+ | Delete a+ deriving (Eq, Ord, Show)++instance Ord a => Delta (DeltaSet1 a) where+ type Base (DeltaSet1 a) = Set a+ apply (Insert a) = Set.insert a+ apply (Delete a) = Set.delete a++-- | Delta type for a 'Set' where+-- collections of elements are inserted or deleted.+data DeltaSet a = DeltaSet+ { inserts :: Set a+ , deletes :: Set a+ -- INVARIANT: The two sets are always disjoint.+ }+ deriving (Eq)++instance Ord a => Delta (DeltaSet a) where+ type Base (DeltaSet a) = Set a+ apply (DeltaSet i d) x = i `Set.union` (x `Set.difference` d)++-- | The smallest delta that changes the second argument to the first argument.+--+-- prop> new = apply (diffSet new old) old+-- prop> diffSet (Set.fromList "ac") (Set.fromList "ab") = deltaSetFromList [Insert 'c', Delete 'b']+diffSet :: Ord a => Set a -> Set a -> DeltaSet a+diffSet new old =+ DeltaSet+ { inserts = new `Set.difference` old+ , deletes = old `Set.difference` new+ }++-- | Flatten a 'DeltaSet' to a list of 'DeltaSet1'.+--+-- In the result list, the set of @a@ appearing as 'Insert'@ a@+-- is /disjoint/ from the set of @a@ appearing as 'Delete'@ a@.+listFromDeltaSet :: DeltaSet a -> [DeltaSet1 a]+listFromDeltaSet DeltaSet{inserts,deletes} =+ map Insert (Set.toList inserts) <> map Delete (Set.toList deletes)++-- | Collect insertions or deletions of elements into a 'DeltaSet'.+--+-- To save space, combinations of 'Insert' and 'Delete'+-- for the same element are simplified when possible.+-- These simplifications always preserve the property+--+-- prop> apply (deltaSetFromList ds) = apply ds+deltaSetFromList :: Ord a => [DeltaSet1 a] -> DeltaSet a+deltaSetFromList = foldr step empty+ where+ empty = DeltaSet Set.empty Set.empty+ step (Insert a) (DeltaSet i d) = DeltaSet (Set.insert a i) (Set.delete a d)+ step (Delete a) (DeltaSet i d) = DeltaSet (Set.delete a i) (Set.insert a d)++-- Note [DeltaSet1 Laws]+{-$DeltaSet1-laws++The following cancellation laws hold:++prop> apply [Insert a, Delete a] = apply (Insert a)+prop> apply [Insert a, Insert a] = apply (Insert a)+prop> apply [Delete a, Insert a] = apply (Delete a)+prop> apply [Delete a, Delete a] = apply (Delete a)++-}++-- | Remember that the semigroup instance is required to satisfy+-- the following properties:+--+-- prop> apply mempty = id+-- prop> apply (d1 <> d2) = apply d1 . apply d2+instance Ord a => Semigroup (DeltaSet a) where+ (DeltaSet i1 d1) <> (DeltaSet i2 d2) = DeltaSet+ (i1 `Set.union` (i2 `Set.difference` d1))+ (d1 `Set.union` (d2 `Set.difference` i1))+ -- This takes into account [DeltaSet1 Cancellations]++instance Ord a => Monoid (DeltaSet a) where+ mempty = DeltaSet Set.empty Set.empty
+ test/unit/Data/Delta/CoreSpec.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Data.Delta.CoreSpec+ ( spec+ ) where++import Prelude++import Data.Delta.Core+ ( Replace (Replace)+ , apply+ )+import Data.Delta.List+ ( DeltaList (Append)+ )+import Test.Hspec+ ( Spec+ , describe+ , it+ )+import Test.QuickCheck+ ( property+ , (===)+ )++{-----------------------------------------------------------------------------+ Tests+------------------------------------------------------------------------------}++spec :: Spec+spec = do+ describe "Replace" $ do+ it "apply is a morphism" $ property $+ \(x :: Int) y z ->+ apply (Replace x <> Replace y) z+ === (apply (Replace x) . apply (Replace y)) z+ + it "apply (Replace x <> _) = apply (Replace x)" $ property $+ \(x :: Int) y z ->+ apply (Replace x <> Replace y) z+ === apply (Replace x) z++ describe "Lists of deltas" $ do+ it "apply []" $ property $+ \(z :: Int) ->+ apply ([] :: [Replace Int]) z === z++ it "apply is a morphism" $ property $+ \xs ys (z :: [Int]) ->+ let d1 = map Append xs+ d2 = map Append ys+ in+ apply (d1 ++ d2) z+ === (apply d1 . apply d2) z
+ test/unit/Data/Delta/EmbeddingSpec.hs view
@@ -0,0 +1,209 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-orphans #-}++{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use lambda-case" #-}++module Data.Delta.EmbeddingSpec+ ( spec+ ) where++import Prelude++import Control.Exception+ ( Exception (..)+ , SomeException+ )+import Data.Delta.Core+ ( Delta (..)+ , Replace (..)+ , apply+ )+import Data.Delta.Embedding+ ( Embedding' (..)+ , Embedding+ , fromEmbedding+ , liftUpdates+ , mkEmbedding+ , pair+ )+import Data.Delta+ ( Semigroupoid (o)+ )+import Data.Maybe+ ( isJust+ )+import Test.Hspec+ ( Spec+ , describe+ , it+ )+import Test.QuickCheck+ ( Arbitrary (..)+ , Property+ , frequency+ , forAll+ , property+ , (===)+ , (.&&.)+ )++{-----------------------------------------------------------------------------+ Tests+------------------------------------------------------------------------------}++spec :: Spec+spec = do+ describe "embeddingAB'" $ do+ it "prop_load_write" $+ prop_load_write embeddingAB'++ it "prop_update_apply" $+ prop_update_apply embeddingAB'++ describe "fromEmbedding . mkEmbedding'" $ do+ let embeddingAB'2 = fromEmbedding $ mkEmbedding embeddingAB'++ it "prop_load_write" $+ prop_load_write embeddingAB'2++ it "prop_update_apply" $+ prop_update_apply embeddingAB'2++ describe "pair" $ do+ let embeddingAABB = fromEmbedding $ pair embeddingAB embeddingAB++ it "prop_load_write" $+ prop_load_write embeddingAABB++ it "prop_update_apply" $+ prop_update_apply embeddingAABB++ describe "liftUpdates" $ do+ it "load . apply" $ property $+ \(das :: [DeltaA]) (a :: A) ->+ let Embedding'{load} = embeddingAB'+ (b, _) = liftUpdates embeddingAB das a+ in toMaybe (load b)+ === Just (apply das a)++ it "apply . load" $ property $+ \(das :: [DeltaA]) (a :: A) ->+ let Embedding'{write} = embeddingAB'+ (b, dbs) = liftUpdates embeddingAB das a+ in b === apply dbs (write a)++ describe "Semigroupid" $ do+ let e1 = diagonal `o` embeddingAB+ e2 = pair embeddingAB embeddingAB `o` diagonal++ it "prop_load_write" $+ prop_load_write (fromEmbedding e1)+ .&&. prop_load_write (fromEmbedding e2)++ it "prop_update_apply" $+ prop_update_apply (fromEmbedding e1)+ .&&. prop_update_apply (fromEmbedding e2)++ it "diagonal commutes" $ property $+ \(das :: [DeltaA]) (a :: A) ->+ let Embedding'{load=load1} = fromEmbedding e1+ Embedding'{load=load2} = fromEmbedding e2+ (b1, _) = liftUpdates e1 das a+ (b2, _) = liftUpdates e2 das a+ in isJust (toMaybe (load1 b1))+ .&&. toMaybe (load1 b1) === toMaybe (load2 b2)++-- | Law relating 'load' and 'write'.+prop_load_write+ :: ( Arbitrary (Base da), Show (Base da), Eq (Base da) )+ => Embedding' da db -> Property+prop_load_write Embedding'{load,write} =+ forAll arbitrary $ \a ->+ toMaybe (load (write a)) === Just a++-- | Law relating 'update' and 'load'.+prop_update_apply+ :: ( Delta da, Delta db, Arbitrary da, Arbitrary (Base da)+ , Show (Base da), Show da, Eq (Base da)+ )+ => Embedding' da db -> Property+prop_update_apply Embedding'{load,write,update} =+ forAll arbitrary $ \a ->+ forAll arbitrary $ \da ->+ let b = write a+ db = update a b da+ in Just (apply da a)+ === toMaybe (load (apply db b))++toMaybe :: Either SomeException b -> Maybe b+toMaybe = either (const Nothing) Just++{-----------------------------------------------------------------------------+ Embeddings+------------------------------------------------------------------------------}+data NoPreimage = NoPreimage+ deriving Show++instance Exception NoPreimage++type A = Int+type DeltaA = Replace Int++type B = Maybe (A, Char)+data DeltaB+ = ChangeNone+ | ChangeA DeltaA+ | ChangeChar Char+ deriving Show++instance Delta DeltaB where+ type Base DeltaB = B+ apply ChangeNone b = b+ apply (ChangeA _ ) Nothing = Nothing+ apply (ChangeA da) (Just (a, c)) = Just (apply da a, c)+ apply (ChangeChar _) Nothing = Nothing+ apply (ChangeChar c) (Just (a, _)) = Just (a, c)++embeddingAB :: Embedding DeltaA DeltaB+embeddingAB = mkEmbedding embeddingAB'++embeddingAB' :: Embedding' DeltaA DeltaB+embeddingAB' = Embedding'+ { load = \b -> case b of+ Nothing -> Left $ toException NoPreimage+ Just (a,_) -> Right a+ , write = \a -> Just (a, 'X')+ , update = \_ _ da -> ChangeA da+ }++-- | Embedding into the diagonal+diagonal :: (Delta da, Eq (Base da)) => Embedding da (da, da)+diagonal = mkEmbedding diagonal'++diagonal' :: (Delta da, Eq (Base da)) => Embedding' da (da, da)+diagonal' = Embedding'+ { load = \(a1, a2) ->+ if a1 == a2+ then Right a1+ else Left $ toException NoPreimage+ , write = \a -> (a, a)+ , update = \_ _ da -> (da, da)+ }++{-----------------------------------------------------------------------------+ Random generators+------------------------------------------------------------------------------}+instance Arbitrary DeltaA where+ arbitrary = Replace <$> arbitrary++instance Arbitrary DeltaB where+ arbitrary = frequency+ [ (1, pure ChangeNone)+ , (4, ChangeA <$> arbitrary)+ , (4, ChangeChar <$> arbitrary)+ ]
+ test/unit/Data/Delta/ListSpec.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Data.Delta.ListSpec+ ( spec+ ) where++import Prelude++import Data.Delta.Core+ ( apply+ )+import Data.Delta.List+ ( DeltaList (Append)+ )+import Test.Hspec+ ( Spec+ , describe+ , it+ )+import Test.QuickCheck+ ( Arbitrary (..)+ , listOf+ , property+ , (===)+ )++{-----------------------------------------------------------------------------+ Tests+------------------------------------------------------------------------------}++spec :: Spec+spec = do+ describe "DeltaList" $ do+ it "apply definition" $ property $+ \(xs :: [Int]) zs ->+ apply (Append xs) zs+ === xs ++ zs++ it "apply mempty" $ property $+ \z ->+ apply (mempty :: DeltaList Int) z+ === z++ it "apply is a morphism" $ property $+ \(x :: DeltaList Int) y zs ->+ apply (x <> y) zs+ === (apply x . apply y) zs++{-----------------------------------------------------------------------------+ Random generators+------------------------------------------------------------------------------}+instance Arbitrary a => Arbitrary (DeltaList a) where+ arbitrary = Append <$> listOf arbitrary
+ test/unit/Data/Delta/SetSpec.hs view
@@ -0,0 +1,121 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Data.Delta.SetSpec+ ( spec+ ) where++import Prelude++import Data.Delta.Core+ ( apply+ )+import Data.Delta.Set+ ( DeltaSet1 (Delete, Insert)+ , deltaSetFromList+ , diffSet+ , listFromDeltaSet+ )+import Data.List+ ( foldl'+ )+import Data.Set+ ( Set+ )+import Test.Hspec+ ( Spec+ , describe+ , it+ )+import Test.QuickCheck+ ( Arbitrary (..)+ , Gen+ , elements+ , forAll+ , infiniteList+ , listOf+ , oneof+ , property+ , (===)+ , (==>)+ , (.&&.)+ )++import qualified Data.Set as Set++{-----------------------------------------------------------------------------+ Tests+------------------------------------------------------------------------------}++spec :: Spec+spec = do+ describe "DeltaSet1" $ do+ it "cancellation laws" $ property $+ \(x :: Int) -> forAll (genSetWithOrWithout x) $ \zs ->+ apply [Insert x, Delete x] zs === apply [Insert x] zs+ .&&. apply [Insert x, Insert x] zs === apply [Insert x] zs+ .&&. apply [Delete x, Insert x] zs === apply [Delete x] zs+ .&&. apply [Delete x, Delete x] zs === apply [Delete x] zs++ describe "DeltaSet" $ do+ describe "diffSet" $ do+ it "example" $ property $+ \(a :: Int) b c ->+ (a /= b && a /= c && b /= c) ==>+ Set.fromList [a, c] `diffSet` Set.fromList [a, b]+ == deltaSetFromList [Insert c, Delete b]++ it "new = apply (diffSet new old) old" $ property $+ \(whole :: Set Int) -> forAll (genSubset whole) $+ \old -> forAll (genSubset whole) $+ \new ->+ new === apply (new `diffSet` old) old++ describe "to/from DeltaSet1" $ do+ it "deltaSetFromList . listFromDeltaSet = id" $ property $+ \(whole :: Set Int) -> forAll (genSubset whole) $+ \a -> forAll (genSubset whole) $+ \b ->+ let d = (a `diffSet` b)+ in d == (deltaSetFromList . listFromDeltaSet) d++ it "apply (deltaSetFromList ds) = apply ds" $ property $+ \(whole :: Set Int) ->+ forAll (genDeltaSet1FromElements whole) $+ \xs -> forAll (genSubset whole) $+ \zs ->+ apply (deltaSetFromList xs) zs+ === apply xs zs++{-----------------------------------------------------------------------------+ Random generators+------------------------------------------------------------------------------}+-- | Generate a 'Set' with equal chances of containing a given item.+genSetWithOrWithout :: (Ord a, Arbitrary a) => a -> Gen (Set a)+genSetWithOrWithout x =+ oneof+ [ Set.insert x <$> arbitrary+ , Set.delete x <$> arbitrary+ ]++-- | Generate a random subset of a given 'Set'.+-- Useful for generating multiple sets that have common elements.+genSubset :: Ord a => Set a -> Gen (Set a)+genSubset xs = do+ isMembers <- infiniteList+ pure+ $ foldl' (flip addMember) Set.empty+ $ zip (Set.toList xs) isMembers+ where+ addMember (x, True) = Set.insert x+ addMember (_, False) = id++-- | Generate a random list of 'DeltaSet1' by picking items from a 'Set'.+genDeltaSet1FromElements :: Set a -> Gen [DeltaSet1 a]+genDeltaSet1FromElements xs+ | Set.null xs = pure []+ | otherwise =+ listOf $ oneof [Insert <$> genElement, Delete <$> genElement]+ where+ genElement = elements $ Set.toList xs
+ test/unit/Main.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}