< User:Dave Menendez(Difference between revisions)
The arrow laws. Should probably be merged into Arrows.
I'm using the formulation from Ross Paterson's "Arrows and Computation", modified for use with more recent libraries. As with MonadPlus, there appear to be no laws for ArrowZero and ArrowPlus.
left identity: id . f = f right identity: f . id = f associativity: f . (g . h) = (f . g) . h
functor-identity: arr id = id functor-composition: arr (g . f) = arr g . arr fFor
extension: first (arr f) = arr (f *** id) functor: first (f . g) = first f . first g exchange: arr (id *** g) . first f = first f . arr (id *** g) unit: arr fst . first f = f . arr fst association: arr assoc . first (first f) = first f . arr assoc
composition: app . arr ((h .) *** id) = h . app reduction: app . arr (mkPair *** id) = id extensionality: app . mkPair f = f
extension: left (arr f) = arr (f +++ id) functor: left (f . g) = left f . left g exchange: arr (id +++ g) . left f = left f . arr (id +++ g) unit: left f . arr Left = arr Left . f association: arr assocsum . left (left f) = left f . arr assocsum distribution: arr distr . first (left f) = left (first f) . arr distr
extension: loop (arr f) = arr (trace f) left tightening: loop (f . first h) = loop f . h right tightening: loop (first h . f) = h . loop f sliding: loop (arr (id *** k) . f) = loop (f . arr (id *** k)) vanishing: loop (loop f) = loop (arr assoc . f . arr unassoc) superposing: second (loop f) = loop (arr unassoc . second f . arr assoc)
6 Utility Functions
assoc :: ((a,b),c) -> (a,(b,c)) assoc ~(~(a,b),c) = (a,(b,c)) unassoc :: (a,(b,c)) -> ((a,b),c) unassoc ~(a,~(b,c)) = ((a,b),c) mkPair :: Arrow a => b -> a c (b,c) mkPair b = arr (\c -> (b,c)) assocsum :: Either (Either a b) c -> Either a (Either b c) assocsum (Left (Left a)) = Left a assocsum (Left (Right b)) = Right (Left b) assocsum (Right c) = Right (Right c) distr :: (Either a b, c) -> Either (a,c) (b,c) distr (Left a, c) = Left (a,c) distr (Right b, c) = Right (b,c) trace :: ((b,d) -> (c,d)) -> b -> c trace f b = let (c,d) = f (b,d) in c