Idris2Doc : Prelude.Interfaces

Prelude.Interfaces

Definitions

interfaceSemigroup : 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 (Maybea)
Semigroup (Lista)
SemigroupString
Semigroup ()
Semigroupa=>Semigroupb=>Semigroup (a, b)
SemigroupOrdering
Semigroupb=>Semigroup (a->b)
(<+>) : Semigroupty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8
interfaceMonoid : 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 (Maybea)
Monoid (Lista)
MonoidString
Monoid ()
Monoida=>Monoidb=>Monoid (a, b)
MonoidOrdering
Monoidb=>Monoid (a->b)
neutral : Monoidty=>ty
Totality: total
Visibility: public export
interfaceFunctor : (Type->Type) ->Type
  Functors allow a uniform action over a parameterised type.
@ f a parameterised type

Parameters: f
Constructor: 
MkFunctor

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

Implementations:
Functor (Paira)
FunctorMaybe
Functor (Eithere)
FunctorList
FunctorStream
FunctorIO
map : Functorf=> (a->b) ->fa->fb
  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
(<$>) : Functorf=> (a->b) ->fa->fb
  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
(<&>) : Functorf=>fa-> (a->b) ->fb
  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
(<$) : Functorf=>b->fa->fb
  Run something for effects, replacing the return value with a given parameter.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4
($>) : Functorf=>fa->b->fb
  Flipped version of `<$`.

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

Totality: total
Visibility: public export
interfaceBifunctor : (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) ->fab->fcd
  The action of the Bifunctor on pairs of morphisms

````idris example
bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")
````
mapFst : (a->c) ->fab->fcb
  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) ->fab->fad
  The action of the Bifunctor on morphisms pertaining to the second object

````idris example
mapSnd reverse (1, "hello") == (1, "olleh")
````

Implementations:
BifunctorPair
BifunctorEither
bimap : Bifunctorf=> (a->c) -> (b->d) ->fab->fcd
  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 : Bifunctorf=> (a->c) ->fab->fcb
  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 : Bifunctorf=> (b->d) ->fab->fad
  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 : Bifunctorf=> (a->b) ->faa->fbb
Totality: total
Visibility: public export
interfaceApplicative : (Type->Type) ->Type
Parameters: f
Constraints: Functor f
Constructor: 
MkApplicative

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

Implementations:
Monoida=>Applicative (Paira)
ApplicativeMaybe
Applicative (Eithere)
ApplicativeList
ApplicativeIO
pure : Applicativef=>a->fa
Totality: total
Visibility: public export
(<*>) : Applicativef=>f (a->b) ->fa->fb
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
(<*) : Applicativef=>fa->fb->fa
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
(*>) : Applicativef=>fa->fb->fb
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
interfaceAlternative : (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 : fa
(<|>) : fa-> Lazy (fa) ->fa
Fixity Declaration: infixr operator, level 2

Implementations:
AlternativeMaybe
AlternativeList
empty : Alternativef=>fa
Totality: total
Visibility: public export
(<|>) : Alternativef=>fa-> Lazy (fa) ->fa
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 2
interfaceMonad : (Type->Type) ->Type
  Monad
@m The underlying functor
A minimal definition includes either `(>>=)` or `join`.

Parameters: m
Constraints: Applicative m
Constructor: 
MkMonad

Methods:
(>>=) : ma-> (a->mb) ->mb
  Also called `bind`.

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

Implementations:
Monoida=>Monad (Paira)
MonadMaybe
Monad (Eithere)
MonadList
MonadIO
(>>=) : Monadm=>ma-> (a->mb) ->mb
  Also called `bind`.

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

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

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

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

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

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

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

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

Totality: total
Visibility: public export
interfaceFoldable : (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->telem->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->telem->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 : telem->Bool
  Test whether the structure is empty.
@ acc The accumulator value which is specified to be lazy
foldlM : Monadm=> (acc->elem->macc) ->acc->telem->macc
  Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
Consequently, the final value is wrapped in the same `Monad`.
toList : telem->Listelem
  Produce a list of the elements contained in the parametrised type.
foldMap : Monoidm=> (a->m) ->ta->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 (Paira)
FoldableMaybe
Foldable (Eithere)
FoldableList
foldr : Foldablet=> (elem->acc->acc) ->acc->telem->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 : Foldablet=> (acc->elem->acc) ->acc->telem->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 : Foldablet=>telem->Bool
  Test whether the structure is empty.
@ acc The accumulator value which is specified to be lazy

Totality: total
Visibility: public export
foldlM : Foldablet=>Monadm=> (acc->elem->macc) ->acc->telem->macc
  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 : Foldablet=>telem->Listelem
  Produce a list of the elements contained in the parametrised type.

Totality: total
Visibility: public export
foldMap : Foldablet=>Monoidm=> (a->m) ->ta->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 : Monoida=>Foldablet=>ta->a
  Combine each element of a structure into a monoid.

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

Totality: total
Visibility: public export
and : Foldablet=>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 : Foldablet=>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 : Foldablet=> (a->Bool) ->ta->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 : Foldablet=> (a->Bool) ->ta->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 : Numa=>Foldablet=>ta->a
  Add together all the elements of a structure.

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

Totality: total
Visibility: export
product : Numa=>Foldablet=>ta->a
  Multiply together all elements of a structure.

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

Totality: total
Visibility: export
traverse_ : Applicativef=>Foldablet=> (a->fb) ->ta->f ()
  Map each element of a structure to a computation, evaluate those
computations and discard the results.

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

Totality: total
Visibility: public export
for_ : Applicativef=>Foldablet=>ta-> (a->fb) ->f ()
  Like `traverse_` but with the arguments flipped.

Totality: total
Visibility: public export
choice : Alternativef=>Foldablet=>t (Lazy (fa)) ->fa
  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 : Alternativef=>Foldablet=> (a->fb) ->ta->fb
  A fused version of `choice` and `map`.

Totality: total
Visibility: public export
interfaceBifoldable : (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->pab->acc
bifoldl : (acc->a->acc) -> (acc->b->acc) ->acc->pab->acc
binull : pab->Bool

Implementations:
BifoldablePair
BifoldableEither
bifoldr : Bifoldablep=> (a->acc->acc) -> (b->acc->acc) ->acc->pab->acc
Totality: total
Visibility: public export
bifoldl : Bifoldablep=> (acc->a->acc) -> (acc->b->acc) ->acc->pab->acc
Totality: total
Visibility: public export
binull : Bifoldablep=>pab->Bool
Totality: total
Visibility: public export
bifoldMap : Monoidacc=>Bifoldablep=> (a->acc) -> (b->acc) ->pab->acc
  Analogous to `foldMap` but for `Bifoldable` structures

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

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

Methods:
traverse : Applicativef=> (a->fb) ->ta->f (tb)
  Map each element of a structure to a computation, evaluate those
computations and combine the results.

Implementations:
Traversable (Paira)
TraversableMaybe
Traversable (Eithere)
TraversableList
traverse : Traversablet=>Applicativef=> (a->fb) ->ta->f (tb)
  Map each element of a structure to a computation, evaluate those
computations and combine the results.

Totality: total
Visibility: public export
sequence : Applicativef=>Traversablet=>t (fa) ->f (ta)
  Evaluate each computation in a structure and collect the results.

Totality: total
Visibility: public export
for : Applicativef=>Traversablet=>ta-> (a->fb) ->f (tb)
  Like `traverse` but with the arguments flipped.

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

Methods:
bitraverse : Applicativef=> (a->fc) -> (b->fd) ->pab->f (pcd)
  Map each element of a structure to a computation, evaluate those
computations and combine the results.

Implementations:
BitraversablePair
BitraversableEither
bitraverse : Bitraversablep=>Applicativef=> (a->fc) -> (b->fd) ->pab->f (pcd)
  Map each element of a structure to a computation, evaluate those
computations and combine the results.

Totality: total
Visibility: public export
bisequence : Applicativef=>Bitraversablep=>p (fa) (fb) ->f (pab)
  Evaluate each computation in a structure and collect the results.

Totality: total
Visibility: public export
bifor : Applicativef=>Bitraversablep=>pab-> (a->fc) -> (b->fd) ->f (pcd)
  Like `bitraverse` but with the arguments flipped.

Totality: total
Visibility: public export