    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Utilities for functors.

    module Agda.Utils.Functor
      ( (<.>)
      , for
      , Decoration(traverseF, distributeF)
      , dmap
      , dget
      -- From Data.Functor:
      , (<$>)
      , ($>)
      , (<&>)
      )
      where

    import Control.Applicative ( Const(Const), getConst )

    import Data.Functor (($>), (<&>))
    import Data.Functor.Identity
    import Data.Functor.Compose

    infixr 9 <.>

    -- | Composition: pure function after functorial (monadic) function.
    (<.>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c
    (b -> c
    f <.> :: forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> a -> m b
    g) a
    a = b -> c
    f (b -> c) -> m b -> m c
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    g a
    a

    -- | The true pure @for@ loop.
    --   'Data.Traversable.for' is a misnomer, it should be @forA@.
    for :: Functor m => m a -> (a -> b) -> m b
    for :: forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for m a
    a a -> b
    b = (a -> b) -> m a -> m b
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    b m a
    a
    {-# INLINE for #-}

    -- | 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@.
    class Functor t => Decoration t where

      -- | @traverseF@ is the defining property.
      traverseF :: Functor m => (a -> m b) -> t a -> m (t b)
      traverseF a -> m b
    f = t (m b) -> m (t b)
    forall (t :: * -> *) (m :: * -> *) a.
    (Decoration t, Functor m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Functor m => t (m a) -> m (t a)
    distributeF (t (m b) -> m (t b)) -> (t a -> t (m b)) -> t a -> m (t b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m b) -> t a -> t (m b)
    forall a b. (a -> b) -> t a -> t b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> m b
    f

      -- | Decorations commute into any functor.
      distributeF :: (Functor m) => t (m a) -> m (t a)
      distributeF = (m a -> m a) -> t (m a) -> m (t a)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Functor m => (a -> m b) -> t a -> m (t b)
    traverseF m a -> m a
    forall a. a -> a
    id

      {-# MINIMAL traverseF | distributeF #-}

    -- | Any decoration is traversable with @traverse = traverseF@.
    --   Just like any 'Traversable' is a functor, so is
    --   any decoration, given by just @traverseF@, a functor.
    dmap :: Decoration t => (a -> b) -> t a -> t b
    dmap :: forall (t :: * -> *) a b. Decoration t => (a -> b) -> t a -> t b
    dmap a -> b
    f = Identity (t b) -> t b
    forall a. Identity a -> a
    runIdentity (Identity (t b) -> t b) -> (t a -> Identity (t b)) -> t a -> t b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Identity b) -> t a -> Identity (t b)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Functor m => (a -> m b) -> t a -> m (t b)
    traverseF (b -> Identity b
    forall a. a -> Identity a
    Identity (b -> Identity b) -> (a -> b) -> a -> Identity b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    f)

    -- | Any decoration is a lens.  @set@ is a special case of @dmap@.
    dget :: Decoration t => t a -> a
    dget :: forall (t :: * -> *) a. Decoration t => t a -> a
    dget = Const a (t (ZonkAny 0)) -> a
    forall {k} a (b :: k). Const a b -> a
    getConst (Const a (t (ZonkAny 0)) -> a)
    -> (t a -> Const a (t (ZonkAny 0))) -> t a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Const a (ZonkAny 0)) -> t a -> Const a (t (ZonkAny 0))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Functor m => (a -> m b) -> t a -> m (t b)
    traverseF a -> Const a (ZonkAny 0)
    forall {k} a (b :: k). a -> Const a b
    Const

    -- | The identity functor is a decoration.
    instance Decoration Identity where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Identity a -> m (Identity b)
    traverseF a -> m b
    f (Identity a
    x) = b -> Identity b
    forall a. a -> Identity a
    Identity (b -> Identity b) -> m b -> m (Identity b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    x

    -- | Decorations compose.  (Thus, they form a category.)
    instance (Decoration d, Decoration t) => Decoration (Compose d t) where
      -- traverseF . traverseF :: Functor m => (a -> m b) -> d (t a) -> m (d (t a))
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Compose d t a -> m (Compose d t b)
    traverseF a -> m b
    f (Compose d (t a)
    x) = d (t b) -> Compose d t b
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (d (t b) -> Compose d t b) -> m (d (t b)) -> m (Compose d t b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (t a -> m (t b)) -> d (t a) -> m (d (t b))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Functor m => (a -> m b) -> d a -> m (d b)
    traverseF ((a -> m b) -> t a -> m (t b)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Functor m => (a -> m b) -> t a -> m (t b)
    traverseF a -> m b
    f) d (t a)
    x

    -- Not a decoration are:
    --
    -- * The constant functor.
    -- * Maybe.  Can only be traversed into pointed functors.
    -- * Other disjoint sum types, like lists etc.
    --   (Can only be traversed into Applicative.)

    -- | A typical decoration is pairing with some stuff.
    instance Decoration ((,) a) where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> (a, a) -> m (a, b)
    traverseF a -> m b
    f (a
    a, a
    x) = (a
    a,) (b -> (a, b)) -> m b -> m (a, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    x