Documentation

Init.Control.Lawful.MonadLift.Basic

LawfulMonadLift and LawfulMonadLiftT #

This module provides classes asserting that MonadLift and MonadLiftT are lawful, which means that monadLift is compatible with pure and bind.

class LawfulMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) [Monad m] [Monad n] [inst : MonadLift m n] :

The MonadLift typeclass only contains the lifting operation. LawfulMonadLift further asserts that lifting commutes with pure and bind:

monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
Instances
    class LawfulMonadLiftT (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n] [inst : MonadLiftT m n] :

    The MonadLiftT typeclass only contains the transitive lifting operation. LawfulMonadLiftT further asserts that lifting commutes with pure and bind:

    monadLift (pure a) = pure a
    monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
    
    Instances