Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Function

Synopsis

- iterate' :: Integral i => i -> (a -> a) -> a -> a
- applyWhen :: IsBool b => b -> (a -> a) -> a -> a
- iterateUntilM :: Monad m => (a -> a -> Bool) -> (a -> m a) -> a -> m a
- applyWhenJust :: Maybe b -> (b -> a -> a) -> a -> a
- applyWhenM :: (IsBool b, Monad m) => m b -> (m a -> m a) -> m a -> m a
- applyUnless :: IsBool b => b -> (a -> a) -> a -> a
- iterWhile :: (b -> Bool) -> (a -> (b, a)) -> a -> [(b, a)]
- repeatWhile :: (a -> (Bool, a)) -> a -> a
- repeatWhileM :: Monad m => (a -> m (Bool, a)) -> a -> m a
- trampolineWhile :: (a -> (Bool, a)) -> a -> a
- trampolineWhileM :: Monad m => (a -> m (Bool, a)) -> a -> m a
- trampoline :: (a -> Either b a) -> a -> b
- trampolineM :: Monad m => (a -> m (Either b a)) -> a -> m b
- iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a
- applyWhenIts :: IsBool b => (a -> b) -> (a -> a) -> a -> a
- applyUnlessIts :: IsBool b => (a -> b) -> (a -> a) -> a -> a
- applyUnlessM :: (IsBool b, Monad m) => m b -> (m a -> m a) -> m a -> m a
- applyWhenNothing :: Maybe b -> (a -> a) -> a -> a
- on :: (b -> b -> c) -> (a -> b) -> a -> a -> c

# Documentation

iterate' :: Integral i => i -> (a -> a) -> a -> a Source #

``iterate'` n f x` applies `f` to `x` `n` times and returns the result.

The applications are calculated strictly.

applyWhen :: IsBool b => b -> (a -> a) -> a -> a Source #

`applyWhen b f a` applies `f` to `a` when `b`.

iterateUntilM :: Monad m => (a -> a -> Bool) -> (a -> m a) -> a -> m a Source #

Monadic version of `iterateUntil`.

applyWhenJust :: Maybe b -> (b -> a -> a) -> a -> a Source #

`Maybe` version of `applyWhen`.

applyWhenM :: (IsBool b, Monad m) => m b -> (m a -> m a) -> m a -> m a Source #

Monadic version of `applyWhen`

applyUnless :: IsBool b => b -> (a -> a) -> a -> a Source #

`applyUnless b f a` applies `f` to `a` unless `b`.

iterWhile :: (b -> Bool) -> (a -> (b, a)) -> a -> [(b, a)] Source #

Repeat a state transition `f :: a -> (b, a)` with output `b` while condition `cond` on the output is true. Return all intermediate results and the final result where `cond` is `False`.

Postconditions (when it terminates): `fst (last (iterWhile cond f a)) == False`. `all fst (init (interWhile cond f a))`.

repeatWhile :: (a -> (Bool, a)) -> a -> a Source #

Repeat something while a condition on some state is true. Return the last state (including the changes of the last transition, even if the condition became false then).

repeatWhileM :: Monad m => (a -> m (Bool, a)) -> a -> m a Source #

Monadic version of `repeatWhile`.

trampolineWhile :: (a -> (Bool, a)) -> a -> a Source #

A version of the trampoline function.

The usual function iterates `f :: a -> Maybe a` as long as `Just{}` is returned, and returns the last value of `a` upon `Nothing`.

`usualTrampoline f = trampolineWhile $ a -> maybe (False,a) (True,) (f a)`.

`trampolineWhile` is very similar to `repeatWhile`, only that it discards the state on which the condition went `False`, and returns the last state on which the condition was `True`.

trampolineWhileM :: Monad m => (a -> m (Bool, a)) -> a -> m a Source #

Monadic version of `trampolineWhile`.

trampoline :: (a -> Either b a) -> a -> b Source #

More general trampoline, which allows some final computation from iteration state `a` into result type `b`.

trampolineM :: Monad m => (a -> m (Either b a)) -> a -> m b Source #

Monadic version of `trampoline`.

iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a Source #

Iteration to fixed-point.

`iterateUntil r f a0` iterates endofunction `f`, starting with `a0`, until `r` relates its result to its input, i.e., `f a `r` a`.

This is the generic pattern behind saturation algorithms.

If `f` is monotone with regard to `r`, meaning `a `r` b` implies `f a `r` f b`, and `f`-chains starting with `a0` are finite then iteration is guaranteed to terminate.

A typical instance will work on sets, and `r` could be set inclusion, and `a0` the empty set, and `f` the step function of a saturation algorithm.

applyWhenIts :: IsBool b => (a -> b) -> (a -> a) -> a -> a Source #

`applyWhenIts p f a` applies `f` to `a` when `p a`.

applyUnlessIts :: IsBool b => (a -> b) -> (a -> a) -> a -> a Source #

`applyUnlessIts p f a` applies `f` to `a` unless `p a`.

applyUnlessM :: (IsBool b, Monad m) => m b -> (m a -> m a) -> m a -> m a Source #

Monadic version of `applyUnless`

applyWhenNothing :: Maybe b -> (a -> a) -> a -> a Source #

`Maybe` version of `applyUnless`.

on :: (b -> b -> c) -> (a -> b) -> a -> a -> c infixl 0 Source #

``on` b u x y` runs the binary function `b` on the results of applying unary function `u` to two arguments `x` and `y`. From the opposite perspective, it transforms two inputs and combines the outputs.

    (op `on` f) x y = f x `op` f y

#### Examples

Expand

    >>> sortBy (compare `on` length) [[0, 1, 2], [0, 1], [], [0]]
    [[],[0],[0,1],[0,1,2]]

    >>> ((+) `on` length) [1, 2, 3] [-1]
    4

    >>> ((,) `on` (*2)) 2 3
    (4,6)

#### Algebraic properties

Expand

-     (*) `on` id = (*) -- (if (*) ∉ {⊥, const ⊥})

-     ((*) `on` f) `on` g = (*) `on` (f . g)

-     flip on f . flip on g = flip on (g . f)