mirror of
https://github.com/coot/free-category.git
synced 2024-09-11 14:17:30 +03:00
Removed Cat type
It's not performing as good as 'Queue' or 'ListTr'.
This commit is contained in:
parent
8501043e10
commit
c5d626e3a5
@ -2,7 +2,8 @@
|
|||||||
[![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)
|
[![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)
|
||||||
[![CircleCI](https://circleci.com/gh/coot/free-category/tree/master.svg?style=svg)](https://circleci.com/gh/coot/free-category/tree/master)
|
[![CircleCI](https://circleci.com/gh/coot/free-category/tree/master.svg?style=svg)](https://circleci.com/gh/coot/free-category/tree/master)
|
||||||
|
|
||||||
This package contains efficient free categories. There are a few presentations based on:
|
This package contains efficient implementation of free categories. There are
|
||||||
|
various resentations available:
|
||||||
|
|
||||||
* real-time queues (C. Okasaki 'Pure Functional Data Structures')
|
* real-time queues (C. Okasaki 'Pure Functional Data Structures')
|
||||||
* type aligned lists
|
* type aligned lists
|
||||||
|
@ -66,30 +66,7 @@ setupEnv500 = replicate 500 [1..500]
|
|||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = defaultMain
|
main = defaultMain
|
||||||
[ env (pure setupEnv100) $ \ints -> bgroup "main"
|
[ env (pure setupEnv100) $ \ints -> bgroup "main"
|
||||||
[ bgroup "Cat 100" $
|
[ bgroup "Queue 100"
|
||||||
[ bench "right right" $
|
|
||||||
whnf
|
|
||||||
(\c -> foldNatCat interpret c 0)
|
|
||||||
(fromListR (liftCat . Add) ints)
|
|
||||||
, bench "right left" $
|
|
||||||
whnf
|
|
||||||
(\c -> foldNatCat interpret c 0)
|
|
||||||
(fromListRL (liftCat . Add) ints)
|
|
||||||
, bench "left left" $
|
|
||||||
whnf
|
|
||||||
(\c -> foldNatCat interpret c 0)
|
|
||||||
(fromListL (liftCat . Add) ints)
|
|
||||||
, bench "left right" $
|
|
||||||
whnf
|
|
||||||
(\c -> foldNatCat interpret c 0)
|
|
||||||
(fromListLR (liftCat . Add) ints)
|
|
||||||
, bench "alternate" $
|
|
||||||
whnf
|
|
||||||
(\c -> foldNatCat interpret c 0)
|
|
||||||
(fromListM (liftCat . Add) ints)
|
|
||||||
]
|
|
||||||
|
|
||||||
, bgroup "Queue 100"
|
|
||||||
[ bench "right right" $
|
[ bench "right right" $
|
||||||
whnf
|
whnf
|
||||||
(\c -> foldNatQ interpret c 0)
|
(\c -> foldNatQ interpret c 0)
|
||||||
@ -159,15 +136,6 @@ main = defaultMain
|
|||||||
]
|
]
|
||||||
]
|
]
|
||||||
, env (pure setupEnv250) $ \ints -> bgroup "main"
|
, env (pure setupEnv250) $ \ints -> bgroup "main"
|
||||||
{--
|
|
||||||
- [ bgroup "Cat 250" $
|
|
||||||
- [ bench "right right" $
|
|
||||||
- whnf
|
|
||||||
- (\c -> foldNatCat interpret c 0)
|
|
||||||
- (fromListR (liftCat . Add) ints)
|
|
||||||
- ]
|
|
||||||
--}
|
|
||||||
|
|
||||||
[ bgroup "Queue 250"
|
[ bgroup "Queue 250"
|
||||||
[ bench "right right" $
|
[ bench "right right" $
|
||||||
whnf
|
whnf
|
||||||
@ -192,15 +160,6 @@ main = defaultMain
|
|||||||
--}
|
--}
|
||||||
]
|
]
|
||||||
, env (pure setupEnv500) $ \ints -> bgroup "main"
|
, env (pure setupEnv500) $ \ints -> bgroup "main"
|
||||||
{--
|
|
||||||
- [ bgroup "Cat 500" $
|
|
||||||
- [ bench "right right" $
|
|
||||||
- whnf
|
|
||||||
- (\c -> foldNatCat interpret c 0)
|
|
||||||
- (fromListR (liftCat . Add) ints)
|
|
||||||
- ]
|
|
||||||
--}
|
|
||||||
|
|
||||||
[ bgroup "Queue 500"
|
[ bgroup "Queue 500"
|
||||||
[ bench "right right" $
|
[ bench "right right" $
|
||||||
whnf
|
whnf
|
||||||
|
@ -1,38 +1,5 @@
|
|||||||
```
|
```
|
||||||
cabal run -O0 bench-cats
|
cabal run -O0 bench-cats
|
||||||
benchmarking main/Cat 100/right right
|
|
||||||
time 2.311 ms (2.243 ms .. 2.442 ms)
|
|
||||||
0.953 R² (0.875 R² .. 0.999 R²)
|
|
||||||
mean 2.300 ms (2.241 ms .. 2.496 ms)
|
|
||||||
std dev 310.7 μs (47.01 μs .. 629.1 μs)
|
|
||||||
variance introduced by outliers: 79% (severely inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/right left
|
|
||||||
time 3.525 ms (3.291 ms .. 3.908 ms)
|
|
||||||
0.930 R² (0.839 R² .. 0.999 R²)
|
|
||||||
mean 3.693 ms (3.503 ms .. 4.401 ms)
|
|
||||||
std dev 982.7 μs (162.3 μs .. 1.995 ms)
|
|
||||||
variance introduced by outliers: 93% (severely inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/left left
|
|
||||||
time 3.454 ms (3.439 ms .. 3.470 ms)
|
|
||||||
1.000 R² (0.999 R² .. 1.000 R²)
|
|
||||||
mean 3.422 ms (3.401 ms .. 3.439 ms)
|
|
||||||
std dev 60.69 μs (42.00 μs .. 89.06 μs)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/left right
|
|
||||||
time 3.397 ms (3.376 ms .. 3.415 ms)
|
|
||||||
1.000 R² (0.999 R² .. 1.000 R²)
|
|
||||||
mean 3.370 ms (3.355 ms .. 3.384 ms)
|
|
||||||
std dev 48.28 μs (38.10 μs .. 63.13 μs)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/alternate
|
|
||||||
time 2.649 ms (2.600 ms .. 2.713 ms)
|
|
||||||
0.998 R² (0.997 R² .. 0.999 R²)
|
|
||||||
mean 2.715 ms (2.692 ms .. 2.737 ms)
|
|
||||||
std dev 76.81 μs (63.80 μs .. 95.94 μs)
|
|
||||||
variance introduced by outliers: 14% (moderately inflated)
|
|
||||||
|
|
||||||
benchmarking main/Queue 100/right right
|
benchmarking main/Queue 100/right right
|
||||||
time 1.141 ms (1.138 ms .. 1.143 ms)
|
time 1.141 ms (1.138 ms .. 1.143 ms)
|
||||||
1.000 R² (1.000 R² .. 1.000 R²)
|
1.000 R² (1.000 R² .. 1.000 R²)
|
||||||
|
@ -1,40 +1,5 @@
|
|||||||
```
|
```
|
||||||
cabal run -O1 bench-cats
|
cabal run -O1 bench-cats
|
||||||
benchmarking main/Cat 100/right right
|
|
||||||
time 383.4 μs (370.0 μs .. 412.2 μs)
|
|
||||||
0.928 R² (0.846 R² .. 0.996 R²)
|
|
||||||
mean 408.5 μs (381.2 μs .. 466.5 μs)
|
|
||||||
std dev 131.4 μs (59.97 μs .. 250.7 μs)
|
|
||||||
variance introduced by outliers: 98% (severely inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/right left
|
|
||||||
time 665.2 μs (647.0 μs .. 681.1 μs)
|
|
||||||
0.996 R² (0.994 R² .. 0.997 R²)
|
|
||||||
mean 651.8 μs (643.7 μs .. 660.0 μs)
|
|
||||||
std dev 27.99 μs (23.84 μs .. 32.75 μs)
|
|
||||||
variance introduced by outliers: 35% (moderately inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/left left
|
|
||||||
time 682.9 μs (671.9 μs .. 692.8 μs)
|
|
||||||
0.997 R² (0.995 R² .. 0.998 R²)
|
|
||||||
mean 694.2 μs (683.5 μs .. 713.7 μs)
|
|
||||||
std dev 46.27 μs (26.75 μs .. 75.32 μs)
|
|
||||||
variance introduced by outliers: 56% (severely inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/left right
|
|
||||||
time 682.0 μs (664.8 μs .. 698.9 μs)
|
|
||||||
0.997 R² (0.995 R² .. 0.998 R²)
|
|
||||||
mean 673.7 μs (666.1 μs .. 682.2 μs)
|
|
||||||
std dev 28.44 μs (24.53 μs .. 33.41 μs)
|
|
||||||
variance introduced by outliers: 34% (moderately inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/alternate
|
|
||||||
ktime 582.0 μs (576.1 μs .. 587.5 μs)
|
|
||||||
0.997 R² (0.995 R² .. 0.999 R²)
|
|
||||||
mean 581.2 μs (573.0 μs .. 597.4 μs)
|
|
||||||
std dev 37.40 μs (21.44 μs .. 68.12 μs)
|
|
||||||
variance introduced by outliers: 56% (severely inflated)
|
|
||||||
|
|
||||||
benchmarking main/Queue 100/right right
|
benchmarking main/Queue 100/right right
|
||||||
time 344.2 μs (337.1 μs .. 362.0 μs)
|
time 344.2 μs (337.1 μs .. 362.0 μs)
|
||||||
0.974 R² (0.923 R² .. 1.000 R²)
|
0.974 R² (0.923 R² .. 1.000 R²)
|
||||||
|
@ -1,39 +1,5 @@
|
|||||||
```
|
```
|
||||||
cabal run -O2 bench-cats
|
cabal run -O2 bench-cats
|
||||||
benchmarking main/Cat 100/right right
|
|
||||||
time 387.7 μs (382.0 μs .. 396.1 μs)
|
|
||||||
0.997 R² (0.992 R² .. 1.000 R²)
|
|
||||||
mean 382.3 μs (378.8 μs .. 389.3 μs)
|
|
||||||
std dev 15.61 μs (9.528 μs .. 27.64 μs)
|
|
||||||
variance introduced by outliers: 35% (moderately inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/right left
|
|
||||||
time 1.902 ms (1.885 ms .. 1.919 ms)
|
|
||||||
0.999 R² (0.999 R² .. 1.000 R²)
|
|
||||||
mean 1.926 ms (1.911 ms .. 1.943 ms)
|
|
||||||
std dev 55.12 μs (41.26 μs .. 90.08 μs)
|
|
||||||
variance introduced by outliers: 15% (moderately inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/left left
|
|
||||||
time 1.941 ms (1.924 ms .. 1.958 ms)
|
|
||||||
0.999 R² (0.999 R² .. 1.000 R²)
|
|
||||||
mean 1.937 ms (1.929 ms .. 1.947 ms)
|
|
||||||
std dev 30.60 μs (23.82 μs .. 41.19 μs)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/left right
|
|
||||||
time 1.946 ms (1.895 ms .. 2.034 ms)
|
|
||||||
0.994 R² (0.988 R² .. 0.999 R²)
|
|
||||||
mean 1.982 ms (1.957 ms .. 2.009 ms)
|
|
||||||
std dev 86.70 μs (66.65 μs .. 112.2 μs)
|
|
||||||
variance introduced by outliers: 30% (moderately inflated)
|
|
||||||
|
|
||||||
benchmarking main/Cat 100/alternate
|
|
||||||
time 1.700 ms (1.605 ms .. 1.902 ms)
|
|
||||||
0.954 R² (0.904 R² .. 1.000 R²)
|
|
||||||
mean 1.641 ms (1.614 ms .. 1.740 ms)
|
|
||||||
std dev 159.2 μs (28.75 μs .. 334.0 μs)
|
|
||||||
variance introduced by outliers: 69% (severely inflated)
|
|
||||||
|
|
||||||
benchmarking main/Queue 100/right right
|
benchmarking main/Queue 100/right right
|
||||||
time 341.9 μs (341.2 μs .. 342.8 μs)
|
time 341.9 μs (341.2 μs .. 342.8 μs)
|
||||||
1.000 R² (1.000 R² .. 1.000 R²)
|
1.000 R² (1.000 R² .. 1.000 R²)
|
||||||
|
@ -23,7 +23,7 @@ import qualified Data.List.NonEmpty as NE
|
|||||||
|
|
||||||
import Test.QuickCheck
|
import Test.QuickCheck
|
||||||
|
|
||||||
import Control.Category.Free (Cat)
|
import Control.Category.Free (ListTr)
|
||||||
|
|
||||||
-- Import classes and combintators used in this example
|
-- Import classes and combintators used in this example
|
||||||
import Control.Category.FreeEffect
|
import Control.Category.FreeEffect
|
||||||
@ -77,16 +77,16 @@ data Tr a (from :: StateType) (to :: StateType) where
|
|||||||
|
|
||||||
login :: Monad m
|
login :: Monad m
|
||||||
=> SStateType st
|
=> SStateType st
|
||||||
-> EffCat m (Cat (Tr a)) 'LoggedOutType st
|
-> EffCat m (ListTr (Tr a)) 'LoggedOutType st
|
||||||
login = liftEffect . Login
|
login = liftEffect . Login
|
||||||
|
|
||||||
logout :: Monad m
|
logout :: Monad m
|
||||||
=> Maybe a
|
=> Maybe a
|
||||||
-> EffCat m (Cat (Tr a)) 'LoggedInType 'LoggedOutType
|
-> EffCat m (ListTr (Tr a)) 'LoggedInType 'LoggedOutType
|
||||||
logout = liftEffect . Logout
|
logout = liftEffect . Logout
|
||||||
|
|
||||||
access :: Monad m
|
access :: Monad m
|
||||||
=> EffCat m (Cat (Tr a)) 'LoggedInType 'LoggedInType
|
=> EffCat m (ListTr (Tr a)) 'LoggedInType 'LoggedInType
|
||||||
access = liftEffect Access
|
access = liftEffect Access
|
||||||
|
|
||||||
--
|
--
|
||||||
@ -168,7 +168,7 @@ accessSecret
|
|||||||
-- @'HandleLogin'@ (with a small modifications) but this way we are able to
|
-- @'HandleLogin'@ (with a small modifications) but this way we are able to
|
||||||
-- test it with a pure @'HandleLogin'@ (see @'handleLoginPure'@).
|
-- test it with a pure @'HandleLogin'@ (see @'handleLoginPure'@).
|
||||||
-> HandleLogin m String a
|
-> HandleLogin m String a
|
||||||
-> EffCat m (Cat (Tr a)) 'LoggedOutType 'LoggedOutType
|
-> EffCat m (ListTr (Tr a)) 'LoggedOutType 'LoggedOutType
|
||||||
accessSecret 0 HandleLogin{handleAccessDenied}
|
accessSecret 0 HandleLogin{handleAccessDenied}
|
||||||
= effect $ handleAccessDenied $> id
|
= effect $ handleAccessDenied $> id
|
||||||
|
|
||||||
@ -183,7 +183,7 @@ accessSecret n HandleLogin{handleLogin}
|
|||||||
where
|
where
|
||||||
handle :: HandleAccess m a
|
handle :: HandleAccess m a
|
||||||
-> Maybe a
|
-> Maybe a
|
||||||
-> EffCat m (Cat (Tr a)) 'LoggedInType 'LoggedOutType
|
-> EffCat m (ListTr (Tr a)) 'LoggedInType 'LoggedOutType
|
||||||
handle LogoutHandler ma = logout ma
|
handle LogoutHandler ma = logout ma
|
||||||
handle (AccessHandler accessHandler dataHandler) _ = effect $ do
|
handle (AccessHandler accessHandler dataHandler) _ = effect $ do
|
||||||
a <- accessHandler
|
a <- accessHandler
|
||||||
|
@ -45,12 +45,6 @@ module Control.Category.Free
|
|||||||
, foldrL
|
, foldrL
|
||||||
, zipWithL
|
, zipWithL
|
||||||
|
|
||||||
-- * Free Category based on Queue
|
|
||||||
, Cat (Id)
|
|
||||||
, liftCat
|
|
||||||
, consCat
|
|
||||||
, foldNatCat
|
|
||||||
|
|
||||||
-- * Free category (CPS style)
|
-- * Free category (CPS style)
|
||||||
, C (..)
|
, C (..)
|
||||||
, liftC
|
, liftC
|
||||||
@ -95,269 +89,6 @@ import Data.Semigroup (Semigroup (..))
|
|||||||
#endif
|
#endif
|
||||||
|
|
||||||
import Control.Category.Free.Internal
|
import Control.Category.Free.Internal
|
||||||
import Unsafe.Coerce (unsafeCoerce)
|
|
||||||
|
|
||||||
|
|
||||||
-- | A version of a free category based on realtime queues. This is an
|
|
||||||
-- optimised version (for right associations) of E.Kemett's free category from
|
|
||||||
-- 'guanxi' project.
|
|
||||||
--
|
|
||||||
-- @('.')@ has @O\(1\)@ complexity, folding is @O\(n\)@ where @n@ is the number
|
|
||||||
-- of transitions.
|
|
||||||
--
|
|
||||||
-- It is optimised for building a morphism from left to right (e.g. with 'foldr' and
|
|
||||||
-- @('.')@). The performance benefits were only seen with @-O1@ or @-O2@,
|
|
||||||
-- though the @-O2@ performance might not be what you expect: morphisms build
|
|
||||||
-- with right fold are fast, but when left folding is used the performance
|
|
||||||
-- drastically decrease (this was not observed with @-O1@).
|
|
||||||
--
|
|
||||||
-- The internal representation is using type aligned 'Queue', a morphism
|
|
||||||
-- `a → c` is represented as a tuple:
|
|
||||||
--
|
|
||||||
-- @
|
|
||||||
-- a → c = ( a → b
|
|
||||||
-- , b ← b₁ : b₂ ← b₃ : ⋯ : bₙ₋₁ ← c : NilQ :: Queue (Cat (Op f) c b)
|
|
||||||
-- )
|
|
||||||
-- @
|
|
||||||
--
|
|
||||||
-- where ← arrows represent arrows in `Cat (Op f)`
|
|
||||||
-- thus we can think of this representation as (though this would not type
|
|
||||||
-- check)
|
|
||||||
--
|
|
||||||
-- @
|
|
||||||
-- a → c ~ ( a → b
|
|
||||||
-- , b → b₁ : b₂ → b₃ : ⋯ : bₙ₋₁ → c : NilQ
|
|
||||||
-- )
|
|
||||||
-- @
|
|
||||||
--
|
|
||||||
-- Type aligned 'Queue's have efficient 'snocQ' and 'unconsQ' operations which
|
|
||||||
-- allow to implement efficient composition and folding for 'Cat'.
|
|
||||||
--
|
|
||||||
-- /Performence/: it does not perform as reliably as 'Queue', which are not
|
|
||||||
-- frigile to left right associations, and it is also more frigile to @-O@
|
|
||||||
-- flags (behaves purly without any optimisations, e.g. @-O0@; and in some
|
|
||||||
-- cases performence degrades with @-O2@ flag).
|
|
||||||
--
|
|
||||||
data Cat (f :: k -> k -> *) a b where
|
|
||||||
Id :: Cat f a a
|
|
||||||
Cat :: Queue (Cat (Op f)) c b
|
|
||||||
-> f a b
|
|
||||||
-> Cat f a c
|
|
||||||
|
|
||||||
compose :: forall (f :: k -> k -> *) x y z.
|
|
||||||
Cat f y z
|
|
||||||
-> Cat f x y
|
|
||||||
-> Cat f x z
|
|
||||||
compose f (Cat q g) = Cat (q `snocQ` op f) g
|
|
||||||
compose Id f = f
|
|
||||||
compose f Id = f
|
|
||||||
{-# INLINE [1] compose #-}
|
|
||||||
|
|
||||||
liftCat :: forall (f :: k -> k -> *) a b.
|
|
||||||
f a b
|
|
||||||
-> Cat f a b
|
|
||||||
liftCat ab = Cat nilQ ab
|
|
||||||
{-# INLINE [1] liftCat #-}
|
|
||||||
|
|
||||||
consCat :: forall (f :: k -> k -> *) a b c.
|
|
||||||
f b c
|
|
||||||
-> Cat f a b
|
|
||||||
-> Cat f a c
|
|
||||||
consCat bc ab = liftCat bc . ab
|
|
||||||
{-# INLINE [1] consCat #-}
|
|
||||||
|
|
||||||
foldNatCat :: forall (f :: k -> k -> *)c a b.
|
|
||||||
Category c
|
|
||||||
=> (forall x y. f x y -> c x y)
|
|
||||||
-> Cat f a b
|
|
||||||
-> c a b
|
|
||||||
foldNatCat _nat Id = id
|
|
||||||
foldNatCat nat (Cat q0 tr0) =
|
|
||||||
case q0 of
|
|
||||||
NilQ -> nat tr0
|
|
||||||
ConsQ Id q' -> go q' . nat tr0
|
|
||||||
ConsQ c q' -> go q' . foldNatCat nat (unOp c) . nat tr0
|
|
||||||
where
|
|
||||||
-- like foldNatQ
|
|
||||||
go :: Queue (Cat (Op f)) x y -> c y x
|
|
||||||
go q = case q of
|
|
||||||
NilQ -> id
|
|
||||||
ConsQ zy q' -> go q' . foldNatCat nat (unOp zy)
|
|
||||||
{-# INLINE [1] foldNatCat #-}
|
|
||||||
|
|
||||||
{-# RULES
|
|
||||||
|
|
||||||
"foldNatCat/consCat"
|
|
||||||
forall (f :: f (v :: k) (w :: k))
|
|
||||||
(q :: Cat f (u :: k) (v :: k))
|
|
||||||
(nat :: forall (x :: k) (y :: k). f x y -> c x y).
|
|
||||||
foldNatCat nat (consCat f q) = nat f . foldNatCat nat q
|
|
||||||
|
|
||||||
"foldNatCat/liftCat"
|
|
||||||
forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
|
|
||||||
(g :: f v w)
|
|
||||||
(h :: Cat f u v).
|
|
||||||
foldNatCat nat (liftCat g `compose` h) = nat g . foldNatCat nat h
|
|
||||||
|
|
||||||
-- TODO: These two rules may never fire due to `Class op` rule.
|
|
||||||
--
|
|
||||||
-- "foldNatCat/foldMap"
|
|
||||||
-- forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
|
|
||||||
-- (fs :: Monoid (c a a) => [f (a :: k) a]).
|
|
||||||
-- foldNatCat nat (foldMap liftCat fs) = foldMap nat fs
|
|
||||||
|
|
||||||
-- "foldNatCat/foldr"
|
|
||||||
-- forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
|
|
||||||
-- (fs :: Monoid (c a a) => [f (a :: k) a])
|
|
||||||
-- (nil :: Cat f a a).
|
|
||||||
-- foldNatCat nat (foldr consCat nil fs) = foldMap nat fs . foldNatCat nat nil
|
|
||||||
|
|
||||||
#-}
|
|
||||||
|
|
||||||
-- | 'op' can be defined as
|
|
||||||
--
|
|
||||||
-- @
|
|
||||||
-- op :: Cat f x y -> Cat (Op f) y x
|
|
||||||
-- op Id = Id
|
|
||||||
-- op (Cat q tr) = Cat nilQ (Op tr) . foldNatQ unDual q
|
|
||||||
-- @
|
|
||||||
--
|
|
||||||
-- where
|
|
||||||
--
|
|
||||||
-- @
|
|
||||||
-- unDual :: forall (f :: k -> k -> *) x y.
|
|
||||||
-- Cat (Op (Op f)) x y
|
|
||||||
-- -> Cat f x y
|
|
||||||
-- unDual Id = Id
|
|
||||||
-- unDual (Cat q (Op (Op tr))) = Cat (hoistQ unDual q) tr
|
|
||||||
-- @
|
|
||||||
--
|
|
||||||
-- But instead we use `unsafeCoerce`, which is safe by the following argument.
|
|
||||||
-- We use `l ~ r` to say that the left and right hand side have the same
|
|
||||||
-- representation. We want to show that `op g ~ g` for any `g :: Cat f x y`
|
|
||||||
--
|
|
||||||
-- It is easy to observe that `unDual g ~ g` for any `x :: Cat (Op (Op f)) x y`.
|
|
||||||
--
|
|
||||||
-- > op Id = Id
|
|
||||||
-- > ~ Id
|
|
||||||
-- > op (Cat q tr)
|
|
||||||
-- > = c₀@(Cat nilQ (Op tr)) . foldNatQ unDual q
|
|
||||||
-- > Note that `.` here denotes composition in `Cat (Op f)`.
|
|
||||||
-- > Let us assume that `q = c₁ : c₂ : ⋯ : cₙ : NilQ`,
|
|
||||||
-- > where each `cᵢ :: Cat (Op (Op tr)) aᵢ aᵢ₊₁`
|
|
||||||
-- > unfolding 'foldNatQ' gives us
|
|
||||||
-- > = c₀ . unDual c₁ . ⋯ . unDual cₙ
|
|
||||||
-- > `unDual cᵢ :: Cat tr aᵢ aᵢ₊₁` has the same representation as cᵢ,
|
|
||||||
-- > at this step we also need to rewrite `.` composition in
|
|
||||||
-- > `Cat (Op f)` using composition in `Cat f`, this reverses the order
|
|
||||||
-- > ~ cₙ . ⋯ . c₁ . Cat nilQ tr
|
|
||||||
-- > By definition of composition in `Cat f`
|
|
||||||
-- > = Cat q tr
|
|
||||||
--
|
|
||||||
-- This proves that `op` does not change the representation and thus it is safe
|
|
||||||
-- to use `unsafeCoerce` instead.
|
|
||||||
--
|
|
||||||
op :: forall (f :: k -> k -> *) x y.
|
|
||||||
Cat f x y
|
|
||||||
-> Cat (Op f) y x
|
|
||||||
op = unsafeCoerce
|
|
||||||
{-# INLINE [1] op #-}
|
|
||||||
|
|
||||||
-- | Since `op` is an identity, it inverse `unOp` must be too. Thus we can
|
|
||||||
-- also use `unsafeCoerce`.
|
|
||||||
--
|
|
||||||
unOp :: forall (f :: k -> k -> *) x y.
|
|
||||||
Cat (Op f) x y
|
|
||||||
-> Cat f y x
|
|
||||||
unOp = unsafeCoerce
|
|
||||||
-- unOp Id = Id
|
|
||||||
-- unOp (Cat q (Op tr)) = Cat nilQ tr . foldNatQ unDual q
|
|
||||||
{-# INLINE [1] unOp #-}
|
|
||||||
|
|
||||||
{-# RULES
|
|
||||||
|
|
||||||
"op/unOp"
|
|
||||||
forall (x :: Cat (Op f) (x :: k) (y :: k)).
|
|
||||||
op (unOp x) = x
|
|
||||||
|
|
||||||
"unOp/op"
|
|
||||||
forall (x :: Cat f (x :: k) (y :: k)).
|
|
||||||
unOp (op x) = x
|
|
||||||
|
|
||||||
#-}
|
|
||||||
|
|
||||||
instance Category (Cat f) where
|
|
||||||
id = Id
|
|
||||||
(.) = compose
|
|
||||||
|
|
||||||
instance Semigroup (Cat f a a) where
|
|
||||||
f <> g = f `compose` g
|
|
||||||
|
|
||||||
instance Monoid (Cat f o o) where
|
|
||||||
mempty = id
|
|
||||||
#if __GLASGOW_HASKELL__ < 804
|
|
||||||
mappend = (<>)
|
|
||||||
#endif
|
|
||||||
|
|
||||||
#if __GLASGOW_HASKELL__ >= 806
|
|
||||||
-- | Show instance via 'ListTr'
|
|
||||||
--
|
|
||||||
instance (forall x y. Show (f x y)) => Show (Cat f a b) where
|
|
||||||
show c = show (hoistFreeH2 c :: ListTr f a b)
|
|
||||||
#else
|
|
||||||
-- | Blind show instance via 'ListTr'
|
|
||||||
--
|
|
||||||
instance Show (Cat f a b) where
|
|
||||||
show c = show (hoistFreeH2 c :: ListTr f a b)
|
|
||||||
#endif
|
|
||||||
|
|
||||||
instance Arrow f => Arrow (Cat f) where
|
|
||||||
arr = liftCat . arr
|
|
||||||
{-# INLINE arr #-}
|
|
||||||
|
|
||||||
Cat q tr *** Cat q' tr' =
|
|
||||||
Cat (zipWithQ (\x y -> op (unOp x *** unOp y)) q q')
|
|
||||||
(tr *** tr')
|
|
||||||
Cat q tr *** Id =
|
|
||||||
Cat (zipWithQ (\x y -> op (unOp x *** unOp y)) q NilQ)
|
|
||||||
(tr *** arr id)
|
|
||||||
Id *** Cat q' tr' =
|
|
||||||
Cat (zipWithQ (\x y -> op (unOp x *** unOp y)) NilQ q')
|
|
||||||
(arr id *** tr')
|
|
||||||
Id *** Id =
|
|
||||||
Cat NilQ (arr id *** arr id)
|
|
||||||
{-# INLINE (***) #-}
|
|
||||||
|
|
||||||
instance ArrowZero f => ArrowZero (Cat f) where
|
|
||||||
zeroArrow = liftCat zeroArrow
|
|
||||||
|
|
||||||
instance ArrowChoice f => ArrowChoice (Cat f) where
|
|
||||||
Cat xb ax +++ Cat yb ay =
|
|
||||||
Cat (zipWithQ (\x y -> op (unOp x +++ unOp y)) xb yb)
|
|
||||||
(ax +++ ay)
|
|
||||||
Cat xb ax +++ Id =
|
|
||||||
Cat (zipWithQ (\x y -> op (unOp x +++ unOp y)) xb NilQ)
|
|
||||||
(ax +++ arr id)
|
|
||||||
Id +++ (Cat xb ax) =
|
|
||||||
Cat (zipWithQ (\x y -> op (unOp x +++ unOp y)) NilQ xb)
|
|
||||||
(arr id +++ ax)
|
|
||||||
Id +++ Id = Id
|
|
||||||
{-# INLINE (+++) #-}
|
|
||||||
|
|
||||||
type instance AlgebraType0 Cat f = ()
|
|
||||||
type instance AlgebraType Cat c = Category c
|
|
||||||
|
|
||||||
-- | /complexity/ of 'foldNatFree2': @O\(n\)@ where @n@ is number of
|
|
||||||
-- transitions embedded in 'Cat'.
|
|
||||||
--
|
|
||||||
instance FreeAlgebra2 Cat where
|
|
||||||
liftFree2 = liftCat
|
|
||||||
{-# INLINE liftFree2 #-}
|
|
||||||
foldNatFree2 = foldNatCat
|
|
||||||
{-# INLINE foldNatFree2 #-}
|
|
||||||
|
|
||||||
codom2 = Proof
|
|
||||||
forget2 = Proof
|
|
||||||
|
|
||||||
|
|
||||||
--
|
--
|
||||||
@ -384,7 +115,7 @@ composeC (C g) (C f) = C $ \k -> g k . f k
|
|||||||
{-# INLINE [1] composeC #-}
|
{-# INLINE [1] composeC #-}
|
||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- Isomorphism from @'Cat'@ to @'C'@, which is a specialisation of
|
-- Isomorphism from @'ListTr'@ to @'C'@, which is a specialisation of
|
||||||
-- @'hoistFreeH2'@.
|
-- @'hoistFreeH2'@.
|
||||||
toC :: ListTr f a b -> C f a b
|
toC :: ListTr f a b -> C f a b
|
||||||
toC = hoistFreeH2
|
toC = hoistFreeH2
|
||||||
|
@ -29,6 +29,7 @@
|
|||||||
module Control.Category.Free.Internal
|
module Control.Category.Free.Internal
|
||||||
( Op (..)
|
( Op (..)
|
||||||
, hoistOp
|
, hoistOp
|
||||||
|
|
||||||
, ListTr (..)
|
, ListTr (..)
|
||||||
, liftL
|
, liftL
|
||||||
, foldNatL
|
, foldNatL
|
||||||
@ -36,6 +37,7 @@ module Control.Category.Free.Internal
|
|||||||
, foldrL
|
, foldrL
|
||||||
, foldlL
|
, foldlL
|
||||||
, zipWithL
|
, zipWithL
|
||||||
|
|
||||||
, Queue (NilQ, ConsQ)
|
, Queue (NilQ, ConsQ)
|
||||||
, liftQ
|
, liftQ
|
||||||
, nilQ
|
, nilQ
|
||||||
|
@ -36,23 +36,20 @@ import Test.Tasty.QuickCheck (testProperty)
|
|||||||
tests :: TestTree
|
tests :: TestTree
|
||||||
tests =
|
tests =
|
||||||
testGroup "Control.Category.Free"
|
testGroup "Control.Category.Free"
|
||||||
[ testProperty "Cat" prop_Cat
|
[ testProperty "Queue" prop_Queue
|
||||||
, testProperty "C" prop_C
|
, testProperty "C" prop_C
|
||||||
, testGroup "Category laws"
|
, testGroup "Category laws"
|
||||||
[ testProperty "Cat id" prop_id_Cat
|
[ testProperty "ListTr id" prop_id_ListTr
|
||||||
, testProperty "Cat associativity" prop_associativity_Cat
|
, testProperty "ListTr associativity" prop_associativity_ListTr
|
||||||
|
, testProperty "Queue id" prop_id_Queue
|
||||||
|
, testProperty "Queue associativity" prop_associativity_Queue
|
||||||
, testProperty "C id" prop_id_C
|
, testProperty "C id" prop_id_C
|
||||||
, testProperty "C associativity" prop_associativity_C
|
, testProperty "C associativity" prop_associativity_C
|
||||||
, testProperty "ListTr id" prop_id_Queue
|
|
||||||
, testProperty "ListTr associativity" prop_associativity_Queue
|
|
||||||
, testProperty "ListTr id" prop_id_ListTr
|
|
||||||
, testProperty "ListTr associativity" prop_associativity_ListTr
|
|
||||||
]
|
]
|
||||||
, testGroup "foldFree2 and foldMap"
|
, testGroup "foldFree2 and foldMap"
|
||||||
[ testProperty "foldFree Cat" prop_foldCat
|
[ testProperty "foldFree ListTr" prop_foldListTr
|
||||||
, testProperty "foldFree C" prop_foldC
|
|
||||||
, testProperty "foldFree Queue" prop_foldQueue
|
, testProperty "foldFree Queue" prop_foldQueue
|
||||||
, testProperty "foldFree ListTr" prop_foldListTr
|
, testProperty "foldFree C" prop_foldC
|
||||||
]
|
]
|
||||||
]
|
]
|
||||||
|
|
||||||
@ -210,20 +207,20 @@ instance Arbitrary ArbListTr where
|
|||||||
--
|
--
|
||||||
-- test 'Cat' and 'C' treating 'ListTr' as a model to compare to.
|
-- test 'Cat' and 'C' treating 'ListTr' as a model to compare to.
|
||||||
--
|
--
|
||||||
prop_Cat, prop_C
|
prop_Queue, prop_C
|
||||||
:: Blind ArbListTr -> Bool
|
:: Blind ArbListTr -> Bool
|
||||||
|
|
||||||
|
|
||||||
prop_Cat (Blind (ArbListTr listTr SInt _)) =
|
prop_Queue (Blind (ArbListTr listTr SInt _)) =
|
||||||
foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
|
||||||
==
|
==
|
||||||
foldNatFree2 interpretTr listTr 0
|
foldNatFree2 interpretTr listTr 0
|
||||||
prop_Cat (Blind (ArbListTr listTr SInteger _)) =
|
prop_Queue (Blind (ArbListTr listTr SInteger _)) =
|
||||||
foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
|
||||||
==
|
==
|
||||||
foldNatFree2 interpretTr listTr 0
|
foldNatFree2 interpretTr listTr 0
|
||||||
prop_Cat (Blind (ArbListTr listTr SNatural _)) =
|
prop_Queue (Blind (ArbListTr listTr SNatural _)) =
|
||||||
foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
|
||||||
==
|
==
|
||||||
foldNatFree2 interpretTr listTr 0
|
foldNatFree2 interpretTr listTr 0
|
||||||
|
|
||||||
@ -311,35 +308,6 @@ toList c = go (hoistFreeH2 c)
|
|||||||
go NilTr = []
|
go NilTr = []
|
||||||
go (ConsTr tr@IntCat{} xs) = tr : go xs
|
go (ConsTr tr@IntCat{} xs) = tr : go xs
|
||||||
|
|
||||||
|
|
||||||
--
|
|
||||||
-- 'Cat' cateogry laws
|
|
||||||
--
|
|
||||||
|
|
||||||
newtype ArbIntCat = ArbIntCat (Cat IntCat '() '())
|
|
||||||
|
|
||||||
instance Show ArbIntCat where
|
|
||||||
show (ArbIntCat c) = show c
|
|
||||||
|
|
||||||
instance Arbitrary ArbIntCat where
|
|
||||||
arbitrary = ArbIntCat . fromList <$> arbitrary
|
|
||||||
shrink (ArbIntCat c) =
|
|
||||||
map (ArbIntCat . fromList)
|
|
||||||
$ shrinkList (const [])
|
|
||||||
$ toList c
|
|
||||||
|
|
||||||
prop_id_Cat :: ArbIntCat -> Bool
|
|
||||||
prop_id_Cat (ArbIntCat f) =
|
|
||||||
prop_id (on (==) toList) f
|
|
||||||
|
|
||||||
prop_associativity_Cat
|
|
||||||
:: ArbIntCat -> ArbIntCat -> ArbIntCat
|
|
||||||
-> Bool
|
|
||||||
prop_associativity_Cat (ArbIntCat f0)
|
|
||||||
(ArbIntCat f1)
|
|
||||||
(ArbIntCat f2) =
|
|
||||||
prop_associativity (on (==) toList) f0 f1 f2
|
|
||||||
|
|
||||||
--
|
--
|
||||||
-- 'C' category laws
|
-- 'C' category laws
|
||||||
--
|
--
|
||||||
@ -429,18 +397,14 @@ prop_associativity_ListTr (ArbIntListTr f0)
|
|||||||
-- Compatibility between 'foldFree2' and 'foldMap' for 'IntCat'
|
-- Compatibility between 'foldFree2' and 'foldMap' for 'IntCat'
|
||||||
--
|
--
|
||||||
|
|
||||||
prop_foldCat :: ArbIntCat -> Bool
|
prop_foldListTr :: ArbIntListTr -> Bool
|
||||||
prop_foldCat (ArbIntCat f)
|
prop_foldListTr (ArbIntListTr f)
|
||||||
= foldFree2 f == foldMap id (toList f)
|
|
||||||
|
|
||||||
prop_foldC :: (Blind ArbIntC) -> Bool
|
|
||||||
prop_foldC (Blind (ArbIntC f))
|
|
||||||
= foldFree2 f == foldMap id (toList f)
|
= foldFree2 f == foldMap id (toList f)
|
||||||
|
|
||||||
prop_foldQueue :: ArbIntQueue -> Bool
|
prop_foldQueue :: ArbIntQueue -> Bool
|
||||||
prop_foldQueue (ArbIntQueue f)
|
prop_foldQueue (ArbIntQueue f)
|
||||||
= foldFree2 f == foldMap id (toList f)
|
= foldFree2 f == foldMap id (toList f)
|
||||||
|
|
||||||
prop_foldListTr :: ArbIntListTr -> Bool
|
prop_foldC :: (Blind ArbIntC) -> Bool
|
||||||
prop_foldListTr (ArbIntListTr f)
|
prop_foldC (Blind (ArbIntC f))
|
||||||
= foldFree2 f == foldMap id (toList f)
|
= foldFree2 f == foldMap id (toList f)
|
||||||
|
Loading…
Reference in New Issue
Block a user