Idris2Doc : Prelude.Interfaces

# Prelude.Interfaces

## Definitions

`interface Semigroup : Type -> Type`
`  Sets equipped with a single binary operation that is associative.  Must  satisfy the following laws:    + Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c`

Parameters: ty
Constructor:
`MkSemigroup`

Methods:
`(<+>) : ty -> ty -> ty`
Fixity Declaration: infixl operator, level 8

Implementations:
`Semigroup (Maybe a)`
`Semigroup (List a)`
`Semigroup String`
`Semigroup ()`
`Semigroup a => Semigroup b => Semigroup (a, b)`
`Semigroup Ordering`
`Semigroup b => Semigroup (a -> b)`
`(<+>) : Semigroup ty => ty -> ty -> ty`
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8
`interface Monoid : Type -> Type`
`  Sets equipped with a single binary operation that is associative, along with  a neutral element for that binary operation.  Must satisfy the following  laws:    + Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Neutral for `<+>`:      forall a, a <+> neutral == a      forall a, neutral <+> a == a`

Parameters: ty
Constraints: Semigroup ty
Constructor:
`MkMonoid`

Methods:
`neutral : ty`

Implementations:
`Monoid (Maybe a)`
`Monoid (List a)`
`Monoid String`
`Monoid ()`
`Monoid a => Monoid b => Monoid (a, b)`
`Monoid Ordering`
`Monoid b => Monoid (a -> b)`
`neutral : Monoid ty => ty`
Totality: total
Visibility: public export
`interface Functor : (Type -> Type) -> Type`
`  Functors allow a uniform action over a parameterised type.  @ f a parameterised type`

Parameters: f
Constructor:
`MkFunctor`

Methods:
`map : (a -> b) -> f a -> f b`
`  Apply a function across everything of type 'a' in a parameterised type  @ f the parameterised type  @ func the function to apply`

Implementations:
`Functor (Pair a)`
`Functor Maybe`
`Functor (Either e)`
`Functor List`
`Functor Stream`
`Functor IO`
`map : Functor f => (a -> b) -> f a -> f b`
`  Apply a function across everything of type 'a' in a parameterised type  @ f the parameterised type  @ func the function to apply`

Totality: total
Visibility: public export
`(<\$>) : Functor f => (a -> b) -> f a -> f b`
`  An infix alias for `map`, applying a function across everything of type 'a'  in a parameterised type.  @ f the parameterised type  @ func the function to apply`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
`(<&>) : Functor f => f a -> (a -> b) -> f b`
`  Flipped version of `<\$>`, an infix alias for `map`, applying a function across  everything of type 'a' in a parameterised type.  @ f the parameterised type  @ func the function to apply`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
`(<\$) : Functor f => b -> f a -> f b`
`  Run something for effects, replacing the return value with a given parameter.`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
`(\$>) : Functor f => f a -> b -> f b`
`  Flipped version of `<\$`.`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
`ignore : Functor f => f a -> f ()`
`  Run something for effects, throwing away the return value.`

Totality: total
Visibility: public export
`interface Bifunctor : (Type -> Type -> Type) -> Type`
`  Bifunctors  @f The action of the Bifunctor on pairs of objects  A minimal definition includes either `bimap` or both `mapFst` and `mapSnd`.`

Parameters: f
Constructor:
`MkBifunctor`

Methods:
`bimap : (a -> c) -> (b -> d) -> f a b -> f c d`
`  The action of the Bifunctor on pairs of morphisms    ````idris example  bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")  ````  `
`mapFst : (a -> c) -> f a b -> f c b`
`  The action of the Bifunctor on morphisms pertaining to the first object    ````idris example  mapFst (\x => x + 1) (1, "hello") == (2, "hello")  ````  `
`mapSnd : (b -> d) -> f a b -> f a d`
`  The action of the Bifunctor on morphisms pertaining to the second object    ````idris example  mapSnd reverse (1, "hello") == (1, "olleh")  ````  `

Implementations:
`Bifunctor Pair`
`Bifunctor Either`
`bimap : Bifunctor f => (a -> c) -> (b -> d) -> f a b -> f c d`
`  The action of the Bifunctor on pairs of morphisms    ````idris example  bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")  ````  `

Totality: total
Visibility: public export
`mapFst : Bifunctor f => (a -> c) -> f a b -> f c b`
`  The action of the Bifunctor on morphisms pertaining to the first object    ````idris example  mapFst (\x => x + 1) (1, "hello") == (2, "hello")  ````  `

Totality: total
Visibility: public export
`mapSnd : Bifunctor f => (b -> d) -> f a b -> f a d`
`  The action of the Bifunctor on morphisms pertaining to the second object    ````idris example  mapSnd reverse (1, "hello") == (1, "olleh")  ````  `

Totality: total
Visibility: public export
`mapHom : Bifunctor f => (a -> b) -> f a a -> f b b`
Totality: total
Visibility: public export
`interface Applicative : (Type -> Type) -> Type`
Parameters: f
Constraints: Functor f
Constructor:
`MkApplicative`

Methods:
`pure : a -> f a`
`(<*>) : f (a -> b) -> f a -> f b`
Fixity Declaration: infixl operator, level 3

Implementations:
`Monoid a => Applicative (Pair a)`
`Applicative Maybe`
`Applicative (Either e)`
`Applicative List`
`Applicative IO`
`pure : Applicative f => a -> f a`
Totality: total
Visibility: public export
`(<*>) : Applicative f => f (a -> b) -> f a -> f b`
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
`(<*) : Applicative f => f a -> f b -> f a`
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
`(*>) : Applicative f => f a -> f b -> f b`
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
`interface Alternative : (Type -> Type) -> Type`
`  An alternative functor has a notion of disjunction.  @f is the underlying applicative functor  We expect (f a, empty, (<|>)) to be a type family of monoids.`

Parameters: f
Constraints: Applicative f
Constructor:
`MkAlternative`

Methods:
`empty : f a`
`(<|>) : f a -> Lazy (f a) -> f a`
Fixity Declaration: infixr operator, level 2

Implementations:
`Alternative Maybe`
`Alternative List`
`empty : Alternative f => f a`
Totality: total
Visibility: public export
`(<|>) : Alternative f => f a -> Lazy (f a) -> f a`
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 2
`interface Monad : (Type -> Type) -> Type`
`  Monad  @m The underlying functor  A minimal definition includes either `(>>=)` or `join`.`

Parameters: m
Constraints: Applicative m
Constructor:
`MkMonad`

Methods:
`(>>=) : m a -> (a -> m b) -> m b`
`  Also called `bind`.`

Fixity Declaration: infixl operator, level 1
`join : m (m a) -> m a`
`  Also called `flatten` or mu.`

Implementations:
`Monoid a => Monad (Pair a)`
`Monad Maybe`
`Monad (Either e)`
`Monad List`
`Monad IO`
`(>>=) : Monad m => m a -> (a -> m b) -> m b`
`  Also called `bind`.`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
`join : Monad m => m (m a) -> m a`
`  Also called `flatten` or mu.`

Totality: total
Visibility: public export
`(=<<) : Monad m => (a -> m b) -> m a -> m b`
`  Right-to-left monadic bind, flipped version of `>>=`.`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
`(>>) : Monad m => m () -> Lazy (m b) -> m b`
`  Sequencing of effectful composition`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
`(>=>) : Monad m => (a -> m b) -> (b -> m c) -> a -> m c`
`  Left-to-right Kleisli composition of monads.`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
`(<=<) : Monad m => (b -> m c) -> (a -> m b) -> a -> m c`
`  Right-to-left Kleisli composition of monads, flipped version of `>=>`.`

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
`guard : Alternative f => Bool -> f ()`
`  `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`.`

Totality: total
Visibility: public export
`when : Applicative f => Bool -> Lazy (f ()) -> f ()`
`  Conditionally execute an applicative expression when the boolean is true.`

Totality: total
Visibility: public export
`unless : Applicative f => Bool -> Lazy (f ()) -> f ()`
`  Execute an applicative expression unless the boolean is true.`

Totality: total
Visibility: public export
`interface Foldable : (Type -> Type) -> Type`
`  The `Foldable` interface describes how you can iterate over the elements in  a parameterised type and combine the elements together, using a provided  function, into a single result.  @ t The type of the 'Foldable' parameterised type.  A minimal definition includes `foldr``

Parameters: t
Constructor:
`MkFoldable`

Methods:
`foldr : (elem -> acc -> acc) -> acc -> t elem -> acc`
`  Successively combine the elements in a parameterised type using the  provided function, starting with the element that is in the final position  i.e. the right-most position.  @ func  The function used to 'fold' an element into the accumulated result  @ init  The starting value the results are being combined into  @ input The parameterised type`
`foldl : (acc -> elem -> acc) -> acc -> t elem -> acc`
`  The same as `foldr` but begins the folding from the element at the initial  position in the data structure i.e. the left-most position.  @ func  The function used to 'fold' an element into the accumulated result  @ init  The starting value the results are being combined into  @ input The parameterised type`
`null : t elem -> Bool`
`  Test whether the structure is empty.  @ acc The accumulator value which is specified to be lazy`
`foldlM : Monad m => (acc -> elem -> m acc) -> acc -> t elem -> m acc`
`  Similar to `foldl`, but uses a function wrapping its result in a `Monad`.  Consequently, the final value is wrapped in the same `Monad`.`
`toList : t elem -> List elem`
`  Produce a list of the elements contained in the parametrised type.`
`foldMap : Monoid m => (a -> m) -> t a -> m`
`  Maps each element to a value and combine them.  For performance reasons, this should wherever  be implemented with tail recursion.  @ f The function to apply to each element.`

Implementations:
`Foldable (Pair a)`
`Foldable Maybe`
`Foldable (Either e)`
`Foldable List`
`foldr : Foldable t => (elem -> acc -> acc) -> acc -> t elem -> acc`
`  Successively combine the elements in a parameterised type using the  provided function, starting with the element that is in the final position  i.e. the right-most position.  @ func  The function used to 'fold' an element into the accumulated result  @ init  The starting value the results are being combined into  @ input The parameterised type`

Totality: total
Visibility: public export
`foldl : Foldable t => (acc -> elem -> acc) -> acc -> t elem -> acc`
`  The same as `foldr` but begins the folding from the element at the initial  position in the data structure i.e. the left-most position.  @ func  The function used to 'fold' an element into the accumulated result  @ init  The starting value the results are being combined into  @ input The parameterised type`

Totality: total
Visibility: public export
`null : Foldable t => t elem -> Bool`
`  Test whether the structure is empty.  @ acc The accumulator value which is specified to be lazy`

Totality: total
Visibility: public export
`foldlM : Foldable t => Monad m => (acc -> elem -> m acc) -> acc -> t elem -> m acc`
`  Similar to `foldl`, but uses a function wrapping its result in a `Monad`.  Consequently, the final value is wrapped in the same `Monad`.`

Totality: total
Visibility: public export
`toList : Foldable t => t elem -> List elem`
`  Produce a list of the elements contained in the parametrised type.`

Totality: total
Visibility: public export
`foldMap : Foldable t => Monoid m => (a -> m) -> t a -> m`
`  Maps each element to a value and combine them.  For performance reasons, this should wherever  be implemented with tail recursion.  @ f The function to apply to each element.`

Totality: total
Visibility: public export
`concat : Monoid a => Foldable t => t a -> a`
`  Combine each element of a structure into a monoid.`

Totality: total
Visibility: public export
`concatMap : Monoid m => Foldable t => (a -> m) -> t a -> m`
`  Combine into a monoid the collective results of applying a function to each  element of a structure.`

Totality: total
Visibility: public export
`and : Foldable t => t (Lazy Bool) -> Bool`
`  The conjunction of all elements of a structure containing lazy boolean  values.  `and` short-circuits from left to right, evaluating until either an  element is `False` or no elements remain.`

Totality: total
Visibility: public export
`or : Foldable t => t (Lazy Bool) -> Bool`
`  The disjunction of all elements of a structure containing lazy boolean  values.  `or` short-circuits from left to right, evaluating either until an  element is `True` or no elements remain.`

Totality: total
Visibility: public export
`any : Foldable t => (a -> Bool) -> t a -> Bool`
`  The disjunction of the collective results of applying a predicate to all  elements of a structure.  `any` short-circuits from left to right.`

Totality: total
Visibility: public export
`all : Foldable t => (a -> Bool) -> t a -> Bool`
`  The conjunction of the collective results of applying a predicate to all  elements of a structure.  `all` short-circuits from left to right.`

Totality: total
Visibility: public export
`sum : Num a => Foldable t => t a -> a`
`  Add together all the elements of a structure.`

Totality: total
Visibility: public export
`sum' : Num a => Foldable t => t a -> a`
`  Add together all the elements of a structure.  Same as `sum` but tail recursive.`

Totality: total
Visibility: export
`product : Num a => Foldable t => t a -> a`
`  Multiply together all elements of a structure.`

Totality: total
Visibility: public export
`product' : Num a => Foldable t => t a -> a`
`  Multiply together all elements of a structure.  Same as `product` but tail recursive.`

Totality: total
Visibility: export
`traverse_ : Applicative f => Foldable t => (a -> f b) -> t a -> f ()`
`  Map each element of a structure to a computation, evaluate those  computations and discard the results.`

Totality: total
Visibility: public export
`sequence_ : Applicative f => Foldable t => t (f a) -> f ()`
`  Evaluate each computation in a structure and discard the results.`

Totality: total
Visibility: public export
`for_ : Applicative f => Foldable t => t a -> (a -> f b) -> f ()`
`  Like `traverse_` but with the arguments flipped.`

Totality: total
Visibility: public export
`choice : Alternative f => Foldable t => t (Lazy (f a)) -> f a`
`  Fold using Alternative.    If you have a left-biased alternative operator `<|>`, then `choice` performs  left-biased choice from a list of alternatives, which means that it  evaluates to the left-most non-`empty` alternative.    If the list is empty, or all values in it are `empty`, then it evaluates to  `empty`.    Example:    ```  -- given a parser expression like:  expr = literal <|> keyword <|> funcall    -- choice lets you write this as:  expr = choice [literal, keyword, funcall]  ```    Note: In Haskell, `choice` is called `asum`.`

Totality: total
Visibility: public export
`choiceMap : Alternative f => Foldable t => (a -> f b) -> t a -> f b`
`  A fused version of `choice` and `map`.`

Totality: total
Visibility: public export
`interface Bifoldable : (Type -> Type -> Type) -> Type`
`  `Bifoldable` identifies foldable structures with two different varieties  of elements (as opposed to `Foldable`, which has one variety of element).  Common examples are `Either` and `Pair`.  A minimal definition includes `bifoldr``

Parameters: p
Constructor:
`MkBifoldable`

Methods:
`bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc`
`bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc`
`binull : p a b -> Bool`

Implementations:
`Bifoldable Pair`
`Bifoldable Either`
`bifoldr : Bifoldable p => (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc`
Totality: total
Visibility: public export
`bifoldl : Bifoldable p => (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc`
Totality: total
Visibility: public export
`binull : Bifoldable p => p a b -> Bool`
Totality: total
Visibility: public export
`bifoldMap : Monoid acc => Bifoldable p => (a -> acc) -> (b -> acc) -> p a b -> acc`
`  Analogous to `foldMap` but for `Bifoldable` structures`

Totality: total
Visibility: public export
`bifoldMapFst : Monoid acc => Bifoldable p => (a -> acc) -> p a b -> acc`
`  Like Bifunctor's `mapFst` but for `Bifoldable` structures`

Totality: total
Visibility: public export
`interface Traversable : (Type -> Type) -> Type`
Parameters: t
Constraints: Functor t, Foldable t
Constructor:
`MkTraversable`

Methods:
`traverse : Applicative f => (a -> f b) -> t a -> f (t b)`
`  Map each element of a structure to a computation, evaluate those  computations and combine the results.`

Implementations:
`Traversable (Pair a)`
`Traversable Maybe`
`Traversable (Either e)`
`Traversable List`
`traverse : Traversable t => Applicative f => (a -> f b) -> t a -> f (t b)`
`  Map each element of a structure to a computation, evaluate those  computations and combine the results.`

Totality: total
Visibility: public export
`sequence : Applicative f => Traversable t => t (f a) -> f (t a)`
`  Evaluate each computation in a structure and collect the results.`

Totality: total
Visibility: public export
`for : Applicative f => Traversable t => t a -> (a -> f b) -> f (t b)`
`  Like `traverse` but with the arguments flipped.`

Totality: total
Visibility: public export
`interface Bitraversable : (Type -> Type -> Type) -> Type`
Parameters: p
Constraints: Bifunctor p, Bifoldable p
Constructor:
`MkBitraversable`

Methods:
`bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)`
`  Map each element of a structure to a computation, evaluate those  computations and combine the results.`

Implementations:
`Bitraversable Pair`
`Bitraversable Either`
`bitraverse : Bitraversable p => Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)`
`  Map each element of a structure to a computation, evaluate those  computations and combine the results.`

Totality: total
Visibility: public export
`bisequence : Applicative f => Bitraversable p => p (f a) (f b) -> f (p a b)`
`  Evaluate each computation in a structure and collect the results.`

Totality: total
Visibility: public export
`bifor : Applicative f => Bitraversable p => p a b -> (a -> f c) -> (b -> f d) -> f (p c d)`
`  Like `bitraverse` but with the arguments flipped.`

Totality: total
Visibility: public export