diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for delta-types + +## 1.0.0.0 — 2025-02-26 + +* Initial version diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 diff --git a/delta-types.cabal b/delta-types.cabal new file mode 100644 --- /dev/null +++ b/delta-types.cabal @@ -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 diff --git a/src/Data/Delta.hs b/src/Data/Delta.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta.hs @@ -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 diff --git a/src/Data/Delta/Core.hs b/src/Data/Delta/Core.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta/Core.hs @@ -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) diff --git a/src/Data/Delta/Embedding.hs b/src/Data/Delta/Embedding.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta/Embedding.hs @@ -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 +-} diff --git a/src/Data/Delta/Embedding/Internal.hs b/src/Data/Delta/Embedding/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta/Embedding/Internal.hs @@ -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)) diff --git a/src/Data/Delta/List.hs b/src/Data/Delta/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta/List.hs @@ -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 [] diff --git a/src/Data/Delta/Map.hs b/src/Data/Delta/Map.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta/Map.hs @@ -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 diff --git a/src/Data/Delta/Set.hs b/src/Data/Delta/Set.hs new file mode 100644 --- /dev/null +++ b/src/Data/Delta/Set.hs @@ -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 diff --git a/test/unit/Data/Delta/CoreSpec.hs b/test/unit/Data/Delta/CoreSpec.hs new file mode 100644 --- /dev/null +++ b/test/unit/Data/Delta/CoreSpec.hs @@ -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 diff --git a/test/unit/Data/Delta/EmbeddingSpec.hs b/test/unit/Data/Delta/EmbeddingSpec.hs new file mode 100644 --- /dev/null +++ b/test/unit/Data/Delta/EmbeddingSpec.hs @@ -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) + ] diff --git a/test/unit/Data/Delta/ListSpec.hs b/test/unit/Data/Delta/ListSpec.hs new file mode 100644 --- /dev/null +++ b/test/unit/Data/Delta/ListSpec.hs @@ -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 diff --git a/test/unit/Data/Delta/SetSpec.hs b/test/unit/Data/Delta/SetSpec.hs new file mode 100644 --- /dev/null +++ b/test/unit/Data/Delta/SetSpec.hs @@ -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 diff --git a/test/unit/Main.hs b/test/unit/Main.hs new file mode 100644 --- /dev/null +++ b/test/unit/Main.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}