Church-encoded Empty & Error carriers #203

robrix · 2019-08-29T14:16:16Z

This PR defines carriers for Empty & Error implemented as Church-encoded monad transformers à la Codensity.

Benchmark against the regular Error carrier.
Tests.
Changelog.
Link from the Error effect.

robrix · 2020-03-15T15:54:03Z

benchmark/Bench/Error.hs

+  [ bench "Either" $ whnf (errorLoop :: Int -> Either Int ()) n
+  , bgroup "Identity"
+    [ bench "Church.ErrorC" $ whnf (run . Church.runError @Int (pure . Left) (pure . Right) . errorLoop) n
+    , bench "Either.ErrorC" $ whnf (run . Either.runError @Int . errorLoop) n
+    , bench "ExceptT"       $ whnf (run . Except.runExceptT @Int . errorLoop) n
+    ]
+  , bgroup "IO"
+    [ bench "Church.ErrorC IO" $ whnfAppIO (Church.runError @Int (pure . Left) (pure . Right) . errorLoop) n
+    , bench "Either.ErrorC IO" $ whnfAppIO (Either.runError @Int . errorLoop) n
+    , bench "ExceptT IO"       $ whnfAppIO (Except.runExceptT @Int . errorLoop) n
+    ]
+  ]


Benchmark results (-O2)

benchmarked Error/Either time 21.15 ms (20.36 ms .. 21.63 ms) 0.996 R² (0.992 R² .. 1.000 R²) mean 22.92 ms (22.33 ms .. 24.41 ms) std dev 1.845 ms (637.7 μs .. 3.254 ms) variance introduced by outliers: 34% (moderately inflated) benchmarked Error/Identity/Church.ErrorC time 47.47 ms (46.94 ms .. 47.98 ms) 1.000 R² (0.999 R² .. 1.000 R²) mean 48.72 ms (48.17 ms .. 49.94 ms) std dev 1.672 ms (858.0 μs .. 2.869 ms) benchmarked Error/Identity/Either.ErrorC time 33.05 ms (32.78 ms .. 33.24 ms) 1.000 R² (0.999 R² .. 1.000 R²) mean 34.26 ms (33.83 ms .. 35.11 ms) std dev 1.253 ms (722.1 μs .. 1.877 ms) variance introduced by outliers: 12% (moderately inflated) benchmarked Error/Identity/ExceptT time 33.26 ms (32.81 ms .. 33.78 ms) 0.999 R² (0.999 R² .. 1.000 R²) mean 34.74 ms (34.17 ms .. 36.11 ms) std dev 1.778 ms (668.9 μs .. 3.034 ms) variance introduced by outliers: 13% (moderately inflated) benchmarked Error/IO/Church.ErrorC IO time 45.44 ms (44.99 ms .. 46.05 ms) 1.000 R² (0.999 R² .. 1.000 R²) mean 46.82 ms (46.32 ms .. 47.98 ms) std dev 1.433 ms (704.4 μs .. 2.344 ms) benchmarked Error/IO/Either.ErrorC IO time 47.49 ms (46.70 ms .. 48.86 ms) 0.998 R² (0.994 R² .. 1.000 R²) mean 49.15 ms (48.31 ms .. 51.28 ms) std dev 2.210 ms (1.225 ms .. 3.408 ms) variance introduced by outliers: 14% (moderately inflated)
benchmarked Error/IO/ExceptT IO time 45.32 ms (44.81 ms .. 45.74 ms) 1.000 R² (0.999 R² .. 1.000 R²) mean 47.76 ms (46.79 ms .. 49.27 ms) std dev 2.341 ms (1.314 ms .. 3.400 ms) variance introduced by outliers: 14% (moderately inflated)

As with all benchmarks, these can be assumed to be lies, but there are a couple of interesting takeaways nonetheless:

You can’t really beat Either because there’s just less for the simplifier to work with. So it’s not necessarily that Either is faster; it’s probably more so that there’s just less code because it’s not a monad transformer. (I’d like to confirm this with a non-transformer Church-encoded Either, but that’s out of scope for this PR.)

ghc can “see through” Identity more easily with Either.ErrorC/ExceptT than with Church.ErrorC.

Church.ErrorC does a little bit better composed onto IO than does Either.ErrorC/ExceptT; this says to me that modulo cases where the simplifier can “see through” some of the types (as with Identity), Church.ErrorC is slightly faster on average.

-O vs. -O2 made a small but noticeable difference.

robrix · 2020-03-15T16:19:42Z

src/Control/Carrier/Empty/Maybe.hs

-- 'runEmpty' ('pure' a) = 'Just' a
+-- 'runEmpty' ('pure' a) = 'pure' ('Just' a)


robrix · 2020-03-15T16:20:13Z

src/Control/Carrier/Error/Church.hs

+-- @
+-- 'runError' j k ('pure' a) = k a
+-- @
+-- @
+-- 'runError' j k ('throwError' e) = j e
+-- @
+-- @
+-- 'runError' j k ('throwError' e \`'catchError'\` 'pure') = k e
+-- @


I’m really happy with how these properties capture the type’s behaviour.

robrix · 2020-03-15T16:20:45Z

src/Control/Carrier/Error/Either.hs

-- 'runError' ('throwError' e `catchError` 'pure') = 'pure' ('Right' e)
+-- 'runError' ('throwError' e \`'catchError'\` 'pure') = 'pure' ('Right' e)


I’ve been meaning to fix this for a while.

robrix · 2020-03-15T16:21:33Z

src/Control/Carrier/NonDet/Church.hs

+-- @
+-- runNonDet fork leaf nil ('pure' a '<|>' 'empty') = leaf a \`fork\` nil
+-- @


I love how this single property completely encapsulates NonDetC’s behaviour w.r.t. its three continuations and the operators they interpret..

robrix · 2020-03-15T16:22:03Z

src/Control/Carrier/Reader.hs

+  liftA2 f (ReaderC a) (ReaderC b) = ReaderC $ \ r ->
+    liftA2 f (a r) (b r)
+  {-# INLINE liftA2 #-}


I’ve implemented liftA2 for a few carriers.

robrix · 2020-03-15T16:25:30Z

src/Control/Carrier/State/Church.hs

-runState :: forall s m a . Applicative m => s -> StateC s m a -> m (s, a)
-runState s (StateC m) = m (\ a s -> pure (s, a)) s
+runState :: forall s m a b . (s -> a -> m b) -> s -> StateC s m a -> m b
+runState f s (StateC m) = m f s


It’s not super important to me that different carriers for the same effect provide exactly the same interface w.r.t. their handlers, and this definition of runState for the Church-encoded StateC is much more flexible.

robrix added 30 commits August 25, 2019 17:04

Stub in a file for a CPS Error carrier.

112b927

Re-export the Error effect & functions.

7c9ae72

Define a CPS error carrier.

b59d46d

Derive a Functor instance for ErrorC.

208af69

Define an Applicative instance for ErrorC.

c91bb38

Define a Monad instance for ErrorC.

e45d5f4

Define a handler for ErrorC.

f852702

Tacit.

7ba67db

Define a MonadTrans instance for ErrorC.

904fd51

Define a MonadFail instance for ErrorC.

c0fac82

Define a MonadIO instance for ErrorC.

488a1f9

Define an Alternative instance for ErrorC.

1691745

Define a MonadPlus instance for ErrorC.

aef7427

Define a MonadFix instance for ErrorC.

1681594

Re-export some things.

a7f845c

Define a Carrier instance for ErrorC.

3f03be3

📝 runError.

78e4b9e

Add the doctest setup block.

d8fc892

Test runError.

c00af0f

Inline all the things.

b569998

Benchmark the two Error carriers against each other.

60f5cea

Inline errorLoop.

3f3d1bc

Inline runError.

754ceed

Give a specialized definition for *>.

9e8c22b

Give a specialized definition for <*.

b9fcfd6

📝 Error.

adc1a02

📝 two laws.

499fa8d

Label the laws.

a67f869

Define a property for the annihilation law.

36c0db1

Define a property for the substitution law.

c24e21b

robrix added 9 commits March 15, 2020 11:15

Move Either out of the Identity group.

ba9babd

Factor out the number of iterations.

7e15e0c

Throw a different error each iteration.

38c2344

10x the iterations.

975a367

Thread in CPS.

2b25981

Fix in CPS.

49df591

🔥 the Cont & CPS carriers.

192560a

Depend on transformers.

2274557

Mention the new Empty carrier in the changelog.

8ff6632

robrix changed the title ~~Church-encoded Error carrier~~ Church-encoded Empty & Error carriers Mar 15, 2020

robrix added 15 commits March 15, 2020 11:56

Correct one of the properties for Maybe.runEmpty.

d8b91e7

Add properties for Church.runEmpty.

6dff900

Prefix all the dependencies with ,.

708de2c

Fix the catchError property for Either.runError.

25396f1

Add properties for Church.runError.

2ab76f6

Simplify the properties using the continuations.

9212fe3

Simplify the Church.runEmpty properties using the continuations.

46b8c89

Simplify the Church.runState properties using the continuation.

bbaa48d

Simplify the Church.evalState & .execState properties.

fe07e2c

Fix a weird heading.

555bb9d

Use run to tidy up a bunch of Church-encoded algebras.

875a6db

Add a property for runNonDet.

5746e55

Add a property for runChoose.

f969272

Add properties for runCut.

eec6198

Define properties for runCull.

2f3222e

robrix commented Mar 15, 2020

View reviewed changes

robrix marked this pull request as ready for review March 15, 2020 16:27

robrix added this to the 1.1.0.0 milestone Mar 15, 2020

robrix merged commit db99b2a into master Mar 15, 2020

robrix deleted the cps-error-carrier branch March 15, 2020 17:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Church-encoded Empty & Error carriers #203

Church-encoded Empty & Error carriers #203

robrix commented Aug 29, 2019 •

edited

robrix Mar 15, 2020

robrix Mar 15, 2020

robrix Mar 15, 2020

robrix Mar 15, 2020

robrix Mar 15, 2020

robrix Mar 15, 2020

robrix Mar 15, 2020

		-- 'runEmpty' ('pure' a) = 'Just' a
		-- 'runEmpty' ('pure' a) = 'pure' ('Just' a)

		-- 'runError' ('throwError' e `catchError` 'pure') = 'pure' ('Right' e)
		-- 'runError' ('throwError' e \`'catchError'\` 'pure') = 'pure' ('Right' e)

Church-encoded Empty & Error carriers #203

Church-encoded Empty & Error carriers #203

Conversation

robrix commented Aug 29, 2019 • edited

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix Mar 15, 2020

Choose a reason for hiding this comment

robrix commented Aug 29, 2019 •

edited