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 ()
  
Semigroup a => Semigroup b => Semigroup (a, b)
  
Semigroup Ordering
  
Semigroup b => Semigroup (a -> b)
  
Semigroup (Maybe a)
  
Semigroup (List a)
  
Semigroup String
(<+>) : 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 ()
  
Monoid a => Monoid b => Monoid (a, b)
  
Monoid Ordering
  
Monoid b => Monoid (a -> b)
  
Monoid (Maybe a)
  
Monoid (List a)
  
Monoid String
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 IO
  
Functor (Pair a)
  
Functor Maybe
  
Functor (Either e)
  
Functor List
  
Functor Stream
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:
  
Applicative IO
  
Monoid a => Applicative (Pair a)
  
Applicative Maybe
  
Applicative (Either e)
  
Applicative List
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:
  
Monad IO
  
Monoid a => Monad (Pair a)
  
Monad Maybe
  
Monad (Either e)
  
Monad List
(>>=) : 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