loop package:base-prelude

The loop operator expresses computations in which an output value is fed back as input, although the computation occurs only once. It underlies the rec value recursion construct in arrow notation. loop should satisfy the following laws:

• extension loop (arr f) = arr (\ b -> fst (fix (\ (c,d) -> f (b,d))))
• left tightening loop (first h >>> f) = h >>> loop f
• right tightening loop (f >>> first h) = loop f >>> h
• sliding loop (f >>> arr (id *** k)) = loop (arr (id *** k) >>> f)
• vanishing loop (loop f) = loop (arr unassoc >>> f >>> arr assoc)
• superposing second (loop f) = loop (arr assoc >>> second f >>> arr unassoc)

where

assoc ((a,b),c) = (a,(b,c))
unassoc (a,(b,c)) = ((a,b),c)