The Functor
typeclass only contains the operations of a functor.
LawfulFunctor
further asserts that these operations satisfy the laws of a functor,
including the preservation of the identity and composition laws:
id <$> x = x
(h ∘ g) <$> x = h <$> g <$> x
Instances
The Applicative
typeclass only contains the operations of an applicative functor.
LawfulApplicative
further asserts that these operations satisfy the laws of an applicative functor:
pure id <*> v = v
pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w)
pure f <*> pure x = pure (f x)
u <*> pure y = pure (· y) <*> u
- seq_assoc {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
Instances
The Monad
typeclass only contains the operations of a monad.
LawfulMonad
further asserts that these operations satisfy the laws of a monad,
including associativity and identity laws for bind
:
pure x >>= f = f x
x >>= pure = x
x >>= f >>= g = x >>= (fun x => f x >>= g)
LawfulMonad.mk'
is an alternative constructor containing useful defaults for many fields.
- seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
Instances
Use simp [← bind_pure_comp]
rather than simp [map_eq_pure_bind]
,
as bind_pure_comp
is in the default simp set, so also using map_eq_pure_bind
would cause a loop.
This is just a duplicate of LawfulApplicative.map_pure
,
but sometimes applies when that doesn't.
It is named with a prime to avoid conflict with the inherited field LawfulMonad.map_pure
.
This is just a duplicate of Functor.map_map
, but sometimes applies when that doesn't.
An alternative constructor for LawfulMonad
which has more
defaultable fields in the common case.