User:Dave Menendez/Arrows

From HaskellWiki

Current revision

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.

1 Category

 left identity:                        id . f = f
 right identity:                       f . id = f
 associativity:                   f . (g . h) = (f . g) . h

2 Arrow

 functor-identity:                     arr id = id
 functor-composition:             arr (g . f) = arr g . arr f

 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

3 ArrowApp

 composition:        app . arr ((h .) *** id) = h . app
 reduction:         app . arr (mkPair *** id) = id
 extensionality:               app . mkPair f = f

4 ArrowChoice

 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

5 ArrowLoop

 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