Skip to content

Commit 6079218

Browse files
TimSheardTimSheard
committed
Introduce Incremental Lambda Calculus, tests, and benchmarks
1 parent a116b2c commit 6079218

File tree

10 files changed

+1151
-3
lines changed

10 files changed

+1151
-3
lines changed

‎libs/cardano-data/cardano-data.cabal

+6-1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ library
2323
Data.UMap
2424
Data.ListMap
2525
Data.Universe
26+
Data.Incremental
2627

2728
hs-source-dirs: src
2829
default-language: Haskell2010
@@ -54,6 +55,7 @@ library testlib
5455

5556
build-depends:
5657
base,
58+
cardano-data,
5759
containers,
5860
hspec,
5961
QuickCheck
@@ -62,7 +64,10 @@ test-suite cardano-data-tests
6264
type: exitcode-stdio-1.0
6365
main-is: Main.hs
6466
hs-source-dirs: test
65-
other-modules: Test.Cardano.Data.MapExtrasSpec
67+
other-modules:
68+
Test.Cardano.Data.MapExtrasSpec
69+
Test.Cardano.Data.Incremental
70+
6671
default-language: Haskell2010
6772
ghc-options:
6873
-Wall -Wcompat -Wincomplete-record-updates

‎libs/cardano-data/src/Data/Incremental.hs

+201
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,201 @@
1+
{-# LANGUAGE BangPatterns #-}
2+
{-# LANGUAGE ConstraintKinds #-}
3+
{-# LANGUAGE DeriveAnyClass #-}
4+
{-# LANGUAGE DeriveGeneric #-}
5+
{-# LANGUAGE DerivingStrategies #-}
6+
{-# LANGUAGE FlexibleContexts #-}
7+
{-# LANGUAGE FlexibleInstances #-}
8+
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
9+
{-# LANGUAGE ScopedTypeVariables #-}
10+
{-# LANGUAGE StandaloneDeriving #-}
11+
{-# LANGUAGE TypeApplications #-}
12+
{-# LANGUAGE TypeFamilies #-}
13+
14+
-- | Introduce the Incremental Lambda Calculus embodied in the ILC class.
15+
-- Instances for two patterns of use involving Maps.
16+
module Data.Incremental where
17+
18+
import Control.DeepSeq (NFData (..))
19+
import Data.Kind
20+
import Data.Map.Internal (Map (..))
21+
import Data.Map.Strict
22+
import qualified Data.Map.Strict as Map
23+
import GHC.Generics (Generic (..))
24+
25+
-- ===================================================
26+
-- Incremental lambda calculus
27+
28+
class ILC t where
29+
data Diff t :: Type
30+
applyDiff :: t -> Diff t -> t
31+
extend :: Diff t -> Diff t -> Diff t
32+
zero :: Diff t
33+
34+
infixr 0 $$
35+
($$) :: ILC t => t -> Diff t -> t
36+
x $$ y = applyDiff x y
37+
38+
-- | Every (Diff t) is a Semigroup
39+
instance ILC t => Semigroup (Diff t) where
40+
x <> y = extend x y
41+
42+
-- | Every (Diff t) is a Monoid
43+
instance ILC t => Monoid (Diff t) where
44+
mempty = zero
45+
46+
-- ==============================================================
47+
-- Delta types.
48+
-- We are going to give the type (Map dom rng) an ILC instance.
49+
-- It turns out there are two reasonable choices for Map. The two
50+
-- reasonable choices differ on what properties the range of the Map
51+
-- has. If the range of the Map is a monoid, there are 3 ways the map
52+
-- might change.
53+
-- 1) entry is deleted,
54+
-- 2) an entry is changed or created, so there is a new range value
55+
-- 3) the range of an entry is combined (using monoid (actually semigroup) <>) with another value.
56+
--
57+
-- If the range is not a Monoid there are only two ways the map might change
58+
-- 1) entry is deleted,
59+
-- 2) an entry is changed or created, so there is a new range value
60+
--
61+
-- To do this we introduce two datatypes MonoidRngD and BinaryRngD. They
62+
-- will become part of the definition for the Diff(Map dom rng). It also
63+
-- turns out thet Both of them are Semigroups (but not Monoids as neither
64+
-- has a notion of No-Change. This is deliberate, but might be reconsidered
65+
-- at some point)
66+
67+
-- | The range is deleted, overwritten, or combined using a Monoid
68+
data MonoidRngD v = Del | Write !v | Comb !v
69+
deriving (Show, Eq, Generic, NFData)
70+
71+
instance (Semigroup t) => Semigroup (MonoidRngD t) where
72+
Del <> Del = Del
73+
Del <> Write _ = Del
74+
Del <> Comb _ = Del
75+
Comb x <> Del = Write x
76+
Comb x <> Write y = Write (x <> y)
77+
Comb x <> Comb y = Comb (x <> y)
78+
Write x <> Del = Write x
79+
Write x <> Comb _ = Write x
80+
Write x <> Write _ = Write x
81+
82+
-- | The range is deleted or changed
83+
data BinaryRngD v = Omit | Edit !v
84+
deriving (Eq, Generic, NFData)
85+
86+
-- The show instance is manual because it supports cutting and pasting
87+
-- error messages, to get values for exploring failures. With out the
88+
-- parantheses they often won't read properly.
89+
instance Show v => Show (BinaryRngD v) where
90+
show Omit = "Omit"
91+
show (Edit d) = "Edit(" ++ show d ++ ")"
92+
93+
instance Semigroup (BinaryRngD t) where
94+
Omit <> Omit = Omit
95+
Omit <> Edit _ = Omit
96+
Edit x <> Omit = Edit x
97+
Edit x <> Edit _ = Edit x
98+
99+
-- ============================================================
100+
-- Since there are two reasonable ILC instances for the Map
101+
-- type we wrap the map in a newtype for the first instance.
102+
-- This is the special case of a Map where the range is a
103+
-- Monoid. We provide tools to enforce the invariant, that in a
104+
-- MonoidMap, we never store 'mempty' of the Monoid.
105+
106+
newtype MonoidMap k v = MM (Map k v)
107+
deriving newtype (Show, Eq, NFData)
108+
109+
unMM :: MonoidMap k v -> Map k v
110+
unMM (MM x) = x
111+
112+
monoidInsertWith :: (Monoid v, Eq v, Ord k) => k -> v -> MonoidMap k v -> MonoidMap k v
113+
monoidInsertWith k !v1 (MM m) = MM (alter ok k m)
114+
where
115+
ok Nothing = if v1 == mempty then Nothing else Just v1
116+
ok (Just v2) = if total == mempty then Nothing else Just total
117+
where
118+
total = v1 <> v2
119+
{-# INLINEABLE monoidInsertWith #-}
120+
121+
monoidInsert :: (Monoid v, Eq v, Ord k) => k -> v -> MonoidMap k v -> MonoidMap k v
122+
monoidInsert k !v1 (MM m) = if v1 == mempty then MM (delete k m) else MM (insert k v1 m)
123+
{-# INLINEABLE monoidInsert #-}
124+
125+
-- =========================================
126+
-- ILC instances
127+
128+
-- | Monoidal maps have special properties, so they get their
129+
-- own instance (wrapped in the newtype).
130+
instance (Ord k, Eq v, ILC v, Monoid v) => ILC (MonoidMap k v) where
131+
newtype Diff (MonoidMap k v) = Dm (Map k (MonoidRngD (Diff v)))
132+
applyDiff mm (Dm md) = Map.foldlWithKey' accum mm md
133+
where
134+
accum :: MonoidMap k v -> k -> MonoidRngD (Diff v) -> MonoidMap k v
135+
accum (MM ans) cred Del = MM (Map.delete cred ans)
136+
accum ans cred (Comb dv) =
137+
monoidInsertWith cred (applyDiff mempty dv) ans
138+
accum ans cred (Write dv) = monoidInsert cred (applyDiff mempty dv) ans
139+
{-# INLINEABLE applyDiff #-}
140+
zero = Dm Map.empty
141+
extend (Dm x) (Dm y) = Dm (Map.unionWith (<>) x y)
142+
143+
instance (Show (Diff v), Show k) => Show (Diff (MonoidMap k v)) where
144+
show (Dm x) = show (Map.toList x)
145+
146+
deriving newtype instance (NFData k, NFData (Diff v)) => NFData (Diff (MonoidMap k v))
147+
148+
-- | Normal map can only be deleted or updated so they use BinaryRngD
149+
instance Ord k => ILC (Map k v) where
150+
newtype Diff (Map k v) = Dn (Map k (BinaryRngD v))
151+
applyDiff m (Dn md) = Map.foldlWithKey' accum m md
152+
where
153+
accum ans k Omit = Map.delete k ans
154+
accum ans k (Edit drep) = Map.insert k drep ans
155+
{-# INLINEABLE applyDiff #-}
156+
zero = Dn Map.empty
157+
extend (Dn x) (Dn y) = Dn (Map.unionWith (<>) x y)
158+
159+
instance (Show k, Show v) => Show (Diff (Map k v)) where
160+
show (Dn x) = show (Map.toList x)
161+
162+
deriving newtype instance (NFData k, NFData v) => NFData (Diff (Map k v))
163+
164+
-- =================================================================
165+
-- helper functions for making binary derivatives
166+
167+
-- | insert a change (MonoidRngD c) into a Map.
168+
-- Note that if we wrap the (result :: Map k (MonoidRngD c)) with the constructor 'Dn'
169+
-- Dn :: Map k (BinaryRngD v) -> Diff (Map k v)
170+
-- then we get Diff(Map k v)
171+
insertC ::
172+
(Ord k, Monoid c) =>
173+
k ->
174+
MonoidRngD c ->
175+
Map k (MonoidRngD c) ->
176+
Map k (MonoidRngD c)
177+
insertC d m x = insertWith (<>) d m x
178+
179+
-- | Split two maps, x and y, into three parts
180+
-- 1) the key appears only in x
181+
-- 2) the key appears in both x and y
182+
-- 3) the key appears only in y
183+
-- Given three 'C'ontinuation style functions, reduce
184+
-- the three parts to a single value.
185+
inter3C ::
186+
Ord k =>
187+
a ->
188+
Map k u ->
189+
Map k v ->
190+
(a -> k -> u -> a) ->
191+
(a -> k -> (u, v) -> a) ->
192+
(a -> k -> v -> a) ->
193+
a
194+
inter3C ans0 m0 n0 c1 c2 c3 = go ans0 m0 n0
195+
where
196+
go ans Tip Tip = ans
197+
go !ans m Tip = Map.foldlWithKey' c1 ans m
198+
go !ans Tip n = Map.foldlWithKey' c3 ans n
199+
go !ans (Bin _ kx x l r) n = case Map.splitLookup kx n of
200+
(ln, Nothing, rn) -> go (go (c1 ans kx x) l ln) r rn
201+
(ln, Just y, rn) -> go (go (c2 ans kx (x, y)) l ln) r rn

‎libs/cardano-data/test/Main.hs

+2
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import System.IO (
77
stdout,
88
utf8,
99
)
10+
import Test.Cardano.Data.Incremental (ilcTests)
1011
import Test.Cardano.Data.MapExtrasSpec (mapExtrasSpec)
1112
import Test.Hspec
1213
import Test.Hspec.Runner
@@ -22,6 +23,7 @@ spec :: Spec
2223
spec =
2324
describe "cardano-data" $ do
2425
describe "MapExtras" mapExtrasSpec
26+
ilcTests
2527

2628
main :: IO ()
2729
main = do

‎libs/cardano-data/test/Test/Cardano/Data/Incremental.hs

+111
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
{-# LANGUAGE FlexibleInstances #-}
2+
{-# LANGUAGE ScopedTypeVariables #-}
3+
{-# LANGUAGE TypeApplications #-}
4+
{-# LANGUAGE TypeFamilies #-}
5+
{-# OPTIONS_GHC -Wno-orphans #-}
6+
7+
module Test.Cardano.Data.Incremental (ilcTests) where
8+
9+
import Data.Incremental
10+
import Data.Map (Map)
11+
import qualified Data.Map.Strict as Map
12+
import Test.Cardano.Data (plusBinary, plusUnary, propExtend, propZero)
13+
import Test.Hspec
14+
import Test.Hspec.QuickCheck
15+
import Test.QuickCheck
16+
17+
-- ==================================================================================
18+
-- These are standins for Coin and DRep which we can't import here
19+
20+
newtype MockCoin = MockCoin Integer
21+
deriving (Eq, Show, Ord)
22+
23+
instance Semigroup MockCoin where
24+
(MockCoin n) <> (MockCoin m) = MockCoin (n + m)
25+
26+
instance Monoid MockCoin where
27+
mempty = MockCoin 0
28+
29+
instance ILC MockCoin where
30+
newtype Diff MockCoin = DeltaMockCoin Integer
31+
deriving (Eq, Show)
32+
applyDiff (MockCoin n) (DeltaMockCoin m) = MockCoin (n + m)
33+
zero = DeltaMockCoin 0
34+
extend (DeltaMockCoin n) (DeltaMockCoin m) = DeltaMockCoin (n + m)
35+
36+
newtype Rep = Rep String
37+
deriving (Eq, Ord, Show)
38+
39+
instance Arbitrary Rep where
40+
arbitrary =
41+
Rep <$> do
42+
a <- choose ('A', 'Z')
43+
b <- choose ('a', 'z')
44+
c <- choose ('0', '9')
45+
pure [a, b, c]
46+
47+
instance Arbitrary (Diff MockCoin) where
48+
arbitrary = DeltaMockCoin <$> arbitrary
49+
50+
instance Arbitrary MockCoin where
51+
arbitrary = MockCoin <$> arbitrary
52+
53+
-- ==================================================================================
54+
-- derivative of a unary function
55+
56+
sumCoins :: Map Int MockCoin -> MockCoin
57+
sumCoins xs = Map.foldl' accum (MockCoin 0) xs
58+
where
59+
accum (MockCoin i) (MockCoin j) = MockCoin (i + j)
60+
61+
sumCoins' :: Map Int MockCoin -> Diff (Map Int MockCoin) -> Diff MockCoin
62+
sumCoins' m (Dn mb) = DeltaMockCoin $ Map.foldlWithKey' accum 0 mb
63+
where
64+
accum ans k Omit = case Map.lookup k m of
65+
Nothing -> ans
66+
Just (MockCoin i) -> ans - i
67+
accum ans k (Edit (MockCoin i)) = case Map.lookup k m of
68+
Nothing -> ans + i
69+
Just (MockCoin j) -> ans + i - j
70+
71+
-- ==================================================================================
72+
-- derivative of a binary function
73+
74+
changeMockCoin :: MockCoin -> MockCoin -> MockCoin
75+
changeMockCoin (MockCoin n) (MockCoin m) = MockCoin (m * n)
76+
77+
changeCoin' :: MockCoin -> Diff MockCoin -> MockCoin -> Diff MockCoin -> Diff MockCoin
78+
changeCoin' (MockCoin n) (DeltaMockCoin i) (MockCoin m) (DeltaMockCoin j) =
79+
DeltaMockCoin (n * j + m * i + i * j)
80+
81+
-- ================================================
82+
-- Property tests
83+
84+
ilcTests :: Spec
85+
ilcTests = describe "ILC tests" $ do
86+
describe "Coin" $ do
87+
propZero (arbitrary @MockCoin)
88+
propExtend (arbitrary @MockCoin) (arbitrary @(Diff MockCoin))
89+
90+
describe "Map cred Coin" $ do
91+
propZero (arbitrary @(Map Int MockCoin))
92+
propExtend (arbitrary @(Map Int MockCoin)) (arbitrary @(Diff (Map Int MockCoin)))
93+
94+
describe "MonoidMap cred Coin" $ do
95+
propZero (arbitrary @(MonoidMap Int MockCoin))
96+
propExtend (arbitrary @(MonoidMap Int MockCoin)) (arbitrary @(Diff (MonoidMap Int MockCoin)))
97+
98+
describe "Map cred Rep" $ do
99+
propZero (arbitrary @(Map Int Rep))
100+
propExtend (arbitrary @(Map Int Rep)) (arbitrary @(Diff (Map Int Rep)))
101+
102+
describe "Unary functions" $
103+
prop "sumCoins' is derivative of unary function sumCoins" $
104+
plusUnary sumCoins sumCoins'
105+
106+
describe "Binary functions" $ do
107+
prop "changeCoin' is derivative of changeCoin" $
108+
plusBinary changeMockCoin changeCoin' arbitrary arbitrary arbitrary arbitrary
109+
110+
-- To run theses tests in ghci, uncomment and type 'main'
111+
-- main = hspec $ ilcTests

0 commit comments

Comments
 (0)