Composition: pure function after functorial (monadic) function.
ModuleAgda-2.7.0.1Haskell2010
Agda.Utils.Functor
Utilities for functors.
- 1 class
- 7 values
- PackageAgda-2.7.0.1
- Exports8
- LanguageHaskell2010
- LicenceMIT
- SourceFunctor.hs
The true pure for loop.
for is a misnomer, it should be forA.
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.
Methods
traverseF :: Functor m => (a -> m b) -> t a -> m (t b)traverseFis the defining property.distributeF :: Functor m => t (m a) -> m (t a)Decorations commute into any functor.
Instances14Decoration, …
Decoration ArgDefined in Agda-2.7.0.1 · Agda.Syntax.CommonDecoration RangedDefined in Agda-2.7.0.1 · Agda.Syntax.CommonDecoration WithHidingDefined in Agda-2.7.0.1 · Agda.Syntax.CommonDecoration WithOriginDefined in Agda-2.7.0.1 · Agda.Syntax.CommonDecoration AbsDefined in Agda-2.7.0.1 · Agda.Syntax.InternalDecoration MaskedDefined in Agda-2.7.0.1 · Agda.Termination.MonadDecoration OpenDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.BaseDecoration IdentityDefined in Agda-2.7.0.1 · Agda.Utils.FunctorThe identity functor is a decoration.
Decoration (Named name)Defined in Agda-2.7.0.1 · Agda.Syntax.CommonDecoration (Dom' t)Defined in Agda-2.7.0.1 · Agda.Syntax.InternalDecoration (Type'' t)Defined in Agda-2.7.0.1 · Agda.Syntax.InternalDecoration (Blocked' t)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.BlockersDecoration (Tuple2 a)Defined in Agda-2.7.0.1 · Agda.Utils.FunctorA typical decoration is pairing with some stuff.
(Decoration d, Decoration t) => Decoration (Compose d t)Defined in Agda-2.7.0.1 · Agda.Utils.FunctorDecorations compose. (Thus, they form a category.)
Any decoration is traversable with traverse = traverseF.
Just like any Traversable is a functor, so is
any decoration, given by just traverseF, a functor.
Any decoration is a lens. set is a special case of dmap.
An infix synonym for fmap.
The name of this operator is an allusion to Prelude.$.
Note the similarities between their types:
($) :: (a -> b) -> a -> b
(<$>) :: Functor f => (a -> b) -> f a -> f bWhereas Prelude.$ is function application, <$> is function
application lifted over a Functor.
Examples
Convert from a Maybe Int to a Maybe
String using show:
show <$> NothingNothing
show <$> Just 3Just "3"
Convert from an Either Int Int to an
Either Int String using show:
show <$> Left 17Left 17
show <$> Right 17Right "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)
Flipped version of <$.
Examples
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")