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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Functor

Description

Utilities for functors.

Synopsis

- (<.>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c
- for :: Functor m => m a -> (a -> b) -> m b
- class Functor t => Decoration (t :: Type -> Type) where
  - traverseF :: Functor m => (a -> m b) -> t a -> m (t b)
  - distributeF :: Functor m => t (m a) -> m (t a)
- dmap :: Decoration t => (a -> b) -> t a -> t b
- dget :: Decoration t => t a -> a
- (<$>) :: Functor f => (a -> b) -> f a -> f b
- ($>) :: Functor f => f a -> b -> f b
- (<&>) :: Functor f => f a -> (a -> b) -> f b

# Documentation

(<.>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c infixr 9 Source #

Composition: pure function after functorial (monadic) function.

for :: Functor m => m a -> (a -> b) -> m b Source #

The true pure `for` loop. `for` is a misnomer, it should be `forA`.

class Functor t => Decoration (t :: Type -> Type) where Source #

A decoration is a functor that is traversable into any functor.

The `Functor` superclass is given because of the limitations of the Haskell class system. `traverseF` actually implies functoriality.

Minimal complete definition: `traverseF` or `distributeF`.

Minimal complete definition

traverseF | distributeF

Methods

traverseF :: Functor m => (a -> m b) -> t a -> m (t b) Source #

`traverseF` is the defining property.

distributeF :: Functor m => t (m a) -> m (t a) Source #

Decorations commute into any functor.

#### Instances

Instances details

Decoration Arg Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Arg a -> m (Arg b) Source # distributeF :: Functor m => Arg (m a) -> m (Arg a) Source #
Decoration Ranged Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Ranged a -> m (Ranged b) Source # distributeF :: Functor m => Ranged (m a) -> m (Ranged a) Source #
Decoration WithHiding Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source # distributeF :: Functor m => WithHiding (m a) -> m (WithHiding a) Source #
Decoration WithOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a) Source #
Decoration Abs Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Abs a -> m (Abs b) Source # distributeF :: Functor m => Abs (m a) -> m (Abs a) Source #
Decoration Masked Source # |
Instance details Defined in Agda.Termination.Monad Methods traverseF :: Functor m => (a -> m b) -> Masked a -> m (Masked b) Source # distributeF :: Functor m => Masked (m a) -> m (Masked a) Source #
Decoration Open Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) Source # distributeF :: Functor m => Open (m a) -> m (Open a) Source #
Decoration Identity Source # | The identity functor is a decoration.
Instance details Defined in Agda.Utils.Functor Methods traverseF :: Functor m => (a -> m b) -> Identity a -> m (Identity b) Source # distributeF :: Functor m => Identity (m a) -> m (Identity a) Source #
Decoration (Named name) Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Named name a -> m (Named name b) Source # distributeF :: Functor m => Named name (m a) -> m (Named name a) Source #
Decoration (Dom' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Dom' t a -> m (Dom' t b) Source # distributeF :: Functor m => Dom' t (m a) -> m (Dom' t a) Source #
Decoration (Type'' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Type'' t a -> m (Type'' t b) Source # distributeF :: Functor m => Type'' t (m a) -> m (Type'' t a) Source #
Decoration (Blocked' t) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods traverseF :: Functor m => (a -> m b) -> Blocked' t a -> m (Blocked' t b) Source # distributeF :: Functor m => Blocked' t (m a) -> m (Blocked' t a) Source #
Decoration ((,) a) Source # | A typical decoration is pairing with some stuff.
Instance details Defined in Agda.Utils.Functor Methods traverseF :: Functor m => (a0 -> m b) -> (a, a0) -> m (a, b) Source # distributeF :: Functor m => (a, m a0) -> m (a, a0) Source #
(Decoration d, Decoration t) => Decoration (Compose d t) Source # | Decorations compose. (Thus, they form a category.)
Instance details Defined in Agda.Utils.Functor Methods traverseF :: Functor m => (a -> m b) -> Compose d t a -> m (Compose d t b) Source # distributeF :: Functor m => Compose d t (m a) -> m (Compose d t a) Source #

dmap :: Decoration t => (a -> b) -> t a -> t b Source #

Any decoration is traversable with `traverse = traverseF`. Just like any `Traversable` is a functor, so is any decoration, given by just `traverseF`, a functor.

dget :: Decoration t => t a -> a Source #

Any decoration is a lens. `set` is a special case of `dmap`.

(<$>) :: Functor f => (a -> b) -> f a -> f b infixl 4 Source #

An infix synonym for `fmap`.

The name of this operator is an allusion to `$`. Note the similarities between their types:

     ($)  ::              (a -> b) ->   a ->   b
    (<$>) :: Functor f => (a -> b) -> f a -> f b

Whereas `$` is function application, `<$>` is function application lifted over a `Functor`.

#### Examples

Expand

Convert from a ``Maybe` `Int`` to a ``Maybe` `String`` using `show`:

    >>> show <$> Nothing
    Nothing

    >>> show <$> Just 3
    Just "3"

Convert from an ``Either` `Int` `Int`` to an ``Either` `Int`` `String` using `show`:

    >>> show <$> Left 17
    Left 17

    >>> show <$> Right 17
    Right "17"

Double each element of a list:

    >>> (*2) <$> [1,2,3]
    [2,4,6]

Apply `even` to the second element of a pair:

    >>> even <$> (2,2)
    (2,True)

($>) :: Functor f => f a -> b -> f b infixl 4 Source #

Flipped version of `<$`.

#### Examples

Expand

Replace the contents of a ``Maybe` `Int`` with a constant `String`:

    >>> Nothing $> "foo"
    Nothing

    >>> Just 90210 $> "foo"
    Just "foo"

Replace the contents of an ``Either` `Int` `Int`` with a constant `String`, resulting in an ``Either` `Int` `String``:

    >>> Left 8675309 $> "foo"
    Left 8675309

    >>> Right 8675309 $> "foo"
    Right "foo"

Replace each element of a list with a constant `String`:

    >>> [1,2,3] $> "foo"
    ["foo","foo","foo"]

Replace the second element of a pair with a constant `String`:

    >>> (1,2) $> "foo"
    (1,"foo")

Since: base-4.7.0.0

(<&>) :: Functor f => f a -> (a -> b) -> f b infixl 1 Source #

Flipped version of `<$>`.

    (<&>) = flip fmap

#### Examples

Expand

Apply `(+1)` to a list, a `Just` and a `Right`:

    >>> Just 2 <&> (+1)
    Just 3

    >>> [1,2,3] <&> (+1)
    [2,3,4]

    >>> Right 3 <&> (+1)
    Right 4

Since: base-4.11.0.0