Skip to content

Commit 62e6efc

Browse files
TimSheardTimSheard
committed
Introduce Incremental Lambda Calculus, tests, and benchmarks
1 parent b3f8866 commit 62e6efc

File tree

10 files changed

+1050
-3
lines changed

10 files changed

+1050
-3
lines changed

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

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ library
2222
Data.MapExtras
2323
Data.UMap
2424
Data.ListMap
25+
Data.Incremental
2526

2627
hs-source-dirs: src
2728
default-language: Haskell2010
@@ -53,6 +54,7 @@ library testlib
5354

5455
build-depends:
5556
base,
57+
cardano-data,
5658
containers,
5759
hspec,
5860
QuickCheck
@@ -61,7 +63,10 @@ test-suite cardano-data-tests
6163
type: exitcode-stdio-1.0
6264
main-is: Main.hs
6365
hs-source-dirs: test
64-
other-modules: Test.Cardano.Data.MapExtrasSpec
66+
other-modules:
67+
Test.Cardano.Data.MapExtrasSpec
68+
Test.Cardano.Data.Incremental
69+
6570
default-language: Haskell2010
6671
ghc-options:
6772
-Wall -Wcompat -Wincomplete-record-updates

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

Lines changed: 181 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
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+
49+
-- | Its is deleted, overwritten, or combined using a Monoid
50+
data MonoidD v = Del | Write !v | Comb !v
51+
deriving (Show, Eq, Generic, NFData)
52+
53+
instance (Semigroup t) => Semigroup (MonoidD t) where
54+
Del <> Del = Del
55+
Del <> Write _ = Del
56+
Del <> Comb _ = Del
57+
Comb x <> Del = Write x
58+
Comb x <> Write y = Write (x <> y)
59+
Comb x <> Comb y = Comb (x <> y)
60+
Write x <> Del = Write x
61+
Write x <> Comb _ = Write x
62+
Write x <> Write _ = Write x
63+
64+
-- | It is deleted or changed
65+
data BinaryD v = Omit | Edit !v
66+
deriving (Eq, Generic, NFData)
67+
68+
instance Show v => Show (BinaryD v) where
69+
show Omit = "Omit"
70+
show (Edit d) = "Edit(" ++ show d ++ ")"
71+
72+
instance Semigroup (BinaryD t) where
73+
Omit <> Omit = Omit
74+
Omit <> Edit _ = Omit
75+
Edit x <> Omit = Edit x
76+
Edit x <> Edit _ = Edit x
77+
78+
-- ======================================================
79+
-- Special case of a Map where the range is a Monoid
80+
-- we provide tools to enforce the invariant, that in a
81+
-- MonoidMap, we never store 'mempty' of the Monoid
82+
83+
newtype MonoidMap k v = MM (Map k v)
84+
deriving newtype (Eq, NFData)
85+
86+
unMM :: MonoidMap k v -> Map k v
87+
unMM (MM x) = x
88+
89+
monoidInsertWith :: (Monoid v, Eq v, Ord k) => k -> v -> MonoidMap k v -> MonoidMap k v
90+
monoidInsertWith k !v1 (MM m) = MM (alter ok k m)
91+
where
92+
ok Nothing = if v1 == mempty then Nothing else Just v1
93+
ok (Just v2) = if total == mempty then Nothing else Just total
94+
where
95+
total = v1 <> v2
96+
{-# INLINEABLE monoidInsertWith #-}
97+
98+
monoidInsert :: (Monoid v, Eq v, Ord k) => k -> v -> MonoidMap k v -> MonoidMap k v
99+
monoidInsert k v1 (MM m) = if v1 == mempty then MM (delete k m) else MM (insert k v1 m)
100+
{-# INLINEABLE monoidInsert #-}
101+
102+
instance (Show k, Show v) => Show (MonoidMap k v) where
103+
show (MM m) = show (Map.toList m)
104+
105+
instance (Show (Diff v), Show k) => Show (Diff (MonoidMap k v)) where
106+
show (Dm x) = show (Map.toList x)
107+
108+
-- =========================================
109+
-- ILC instances
110+
111+
-- | Monoidal maps have special properties, so they get their
112+
-- own instance (wrapped in the newtype).
113+
instance (Ord k, Eq v, ILC v, Monoid v) => ILC (MonoidMap k v) where
114+
newtype Diff (MonoidMap k v) = Dm (Map k (MonoidD (Diff v)))
115+
applyDiff mm (Dm md) = Map.foldlWithKey' accum mm md
116+
where
117+
accum :: MonoidMap k v -> k -> MonoidD (Diff v) -> MonoidMap k v
118+
accum (MM ans) cred Del = MM (Map.delete cred ans)
119+
accum ans cred (Comb dv) =
120+
monoidInsertWith cred (applyDiff mempty dv) ans
121+
accum ans cred (Write dv) = monoidInsert cred (applyDiff mempty dv) ans
122+
{-# INLINEABLE applyDiff #-}
123+
zero = Dm Map.empty
124+
extend (Dm x) (Dm y) = Dm (Map.unionWith (<>) x y)
125+
126+
deriving newtype instance (NFData k, NFData (Diff v)) => NFData (Diff (MonoidMap k v))
127+
128+
-- | Normal map can only be deleted or updated so they use BinaryD
129+
instance Ord k => ILC (Map k v) where
130+
newtype Diff (Map k v) = Dn (Map k (BinaryD v))
131+
applyDiff m (Dn md) = Map.foldlWithKey' accum m md
132+
where
133+
accum ans k Omit = Map.delete k ans
134+
accum ans k (Edit drep) = Map.insert k drep ans
135+
{-# INLINEABLE applyDiff #-}
136+
zero = Dn Map.empty
137+
extend (Dn x) (Dn y) = Dn (Map.unionWith (<>) x y)
138+
139+
instance (Show k, Show v) => Show (Diff (Map k v)) where
140+
show (Dn x) = show (Map.toList x)
141+
142+
deriving newtype instance (NFData k, NFData v) => NFData (Diff (Map k v))
143+
144+
-- =================================================================
145+
-- helper functions for making binary derivatives
146+
147+
-- | insert a change (MonoidD c) into a Map.
148+
-- Note that if we wrap the (result :: Map k (MonoidD c)) with the constructor 'Dn'
149+
-- Dn :: Map k (BinaryD v) -> Diff (Map k v)
150+
-- then we get Diff(Map k v)
151+
insertC ::
152+
(Ord k, Monoid c) =>
153+
k ->
154+
MonoidD c ->
155+
Map k (MonoidD c) ->
156+
Map k (MonoidD c)
157+
insertC d m x = insertWith (<>) d m x
158+
159+
-- | Split two maps, x and y, into three parts
160+
-- 1) the key appears only in x
161+
-- 2) the key appears in both x and y
162+
-- 3) the key appears only in y
163+
-- Given three 'C'ontinuation style functions, reduce
164+
-- the three parts to a single value.
165+
inter3C ::
166+
Ord k =>
167+
a ->
168+
Map k u ->
169+
Map k v ->
170+
(a -> k -> u -> a) ->
171+
(a -> k -> (u, v) -> a) ->
172+
(a -> k -> v -> a) ->
173+
a
174+
inter3C ans0 m0 n0 c1 c2 c3 = go ans0 m0 n0
175+
where
176+
go ans Tip Tip = ans
177+
go ans m Tip = (Map.foldlWithKey' c1 ans m)
178+
go ans Tip n = (Map.foldlWithKey' c3 ans n)
179+
go ans (Bin _ kx x l r) n = case Map.splitLookup kx n of
180+
(ln, Nothing, rn) -> go (go (c1 ans kx x) l ln) r rn
181+
(ln, Just y, rn) -> go (go (c2 ans kx (x, y)) l ln) r rn

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

Lines changed: 2 additions & 0 deletions
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

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
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 Data.Monoid (Sum (..))
13+
import Test.Cardano.Data (plusBinary, plusUnary, propExtend, propZero)
14+
import Test.Hspec
15+
import Test.Hspec.QuickCheck
16+
import Test.QuickCheck
17+
18+
-- ==================================================================================
19+
-- These are standins for Coin and DRep which we can't import here
20+
21+
type Coin = Sum Integer
22+
23+
instance ILC (Sum Integer) where
24+
newtype Diff (Sum Integer) = DeltaSum Integer
25+
deriving (Eq, Show)
26+
applyDiff (Sum n) (DeltaSum m) = Sum (n + m)
27+
zero = DeltaSum 0
28+
extend (DeltaSum n) (DeltaSum m) = DeltaSum (n + m)
29+
30+
newtype Rep = Rep String
31+
deriving (Eq, Ord, Show)
32+
33+
instance Arbitrary Rep where
34+
arbitrary =
35+
Rep <$> do
36+
a <- choose ('A', 'Z')
37+
b <- choose ('a', 'z')
38+
c <- choose ('0', '9')
39+
pure [a, b, c]
40+
41+
instance Arbitrary (Diff (Sum Integer)) where
42+
arbitrary = DeltaSum <$> arbitrary
43+
44+
-- ==================================================================================
45+
-- derivative of a unary function
46+
47+
sumCoins :: Map Int Coin -> Coin
48+
sumCoins xs = Map.foldl' accum (Sum 0) xs
49+
where
50+
accum (Sum i) (Sum j) = Sum (i + j)
51+
52+
sumCoins' :: Map Int Coin -> Diff (Map Int Coin) -> Diff Coin
53+
sumCoins' m (Dn mb) = DeltaSum $ Map.foldlWithKey' accum 0 mb
54+
where
55+
accum ans k Omit = case Map.lookup k m of
56+
Nothing -> ans
57+
Just (Sum i) -> ans - i
58+
accum ans k (Edit (Sum i)) = case Map.lookup k m of
59+
Nothing -> ans + i
60+
Just (Sum j) -> ans + i - j
61+
62+
-- ==================================================================================
63+
-- derivative of a binary function
64+
65+
changeCoin :: Coin -> Coin -> Coin
66+
changeCoin (Sum n) (Sum m) = Sum (m * n)
67+
68+
changeCoin' :: Coin -> Diff Coin -> Coin -> Diff Coin -> Diff Coin
69+
changeCoin' (Sum n) (DeltaSum i) (Sum m) (DeltaSum j) =
70+
DeltaSum (n * j + m * i + i * j)
71+
72+
-- ================================================
73+
-- Property tests
74+
75+
ilcTests :: Spec
76+
ilcTests = describe "ILC tests" $ do
77+
describe "Coin" $ do
78+
propZero (arbitrary @Coin)
79+
propExtend (arbitrary @Coin) (arbitrary @(Diff Coin))
80+
81+
describe "Map cred Coin" $ do
82+
propZero (arbitrary @(Map Int Coin))
83+
propExtend (arbitrary @(Map Int Coin)) (arbitrary @(Diff (Map Int Coin)))
84+
85+
describe "MonoidMap cred Coin" $ do
86+
propZero (arbitrary @(MonoidMap Int Coin))
87+
propExtend (arbitrary @(MonoidMap Int Coin)) (arbitrary @(Diff (MonoidMap Int Coin)))
88+
89+
describe "Map cred Rep" $ do
90+
propZero (arbitrary @(Map Int Rep))
91+
propExtend (arbitrary @(Map Int Rep)) (arbitrary @(Diff (Map Int Rep)))
92+
93+
describe "Unary functions" $
94+
prop "sumCoins' is derivative of unary function sumCoins" $
95+
plusUnary sumCoins sumCoins'
96+
97+
describe "Binary functions" $ do
98+
prop "changeCoin' is derivative of changeCoin" $
99+
plusBinary changeCoin changeCoin' arbitrary arbitrary arbitrary arbitrary

0 commit comments

Comments
 (0)