# User:Dave Menendez/Arrows

< User:Dave Menendez

Jump to navigation
Jump to search
Revision as of 06:03, 21 May 2010 by Dave Menendez (talk | contribs)

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.

## Category

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

## Arrow

For `arr`

:

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

For `first`

:

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

## ArrowApp

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

## 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

## 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)

## 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
```