-- | Utilities for functors.

module Agda.Utils.Functor
  ( (<.>)
  , for
  , Decoration(traverseF, distributeF)
  , dmap
  , dget
  -- From Data.Functor:
  , (<$>)
  , ($>)
  -- Defined identically as in Data.Functor.
  -- Should be simply re-exported (vs redefined) once
  -- MIN_VERSION_base >= 4.11.0.0
  -- At time of this writing, we support 4.9.0.0.
  , (<&>)
  )
  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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
b m a
a
{-# INLINE for #-}

infixl 1 <&>

-- | Infix version of 'for'.
(<&>) :: Functor m => m a -> (a -> b) -> m b
<&> :: forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
(<&>) m a
a a -> b
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 (<&>) #-}

-- | 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)
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 (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)
traverseF m a -> m a
forall a. a -> a
id

-- | 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)
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 Any) -> a
forall {k} a (b :: k). Const a b -> a
getConst (Const a (t Any) -> a) -> (t a -> Const a (t Any)) -> t a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Const a Any) -> t a -> Const a (t Any)
forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF a -> Const a Any
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)
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)
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