Lake.Util.EquipT

def Lake.EquipT (ρ : Type u) (m : Type v → Type w) (α : Type v) :

Type (max u w)

A monad transformer that equips a monad with a value. This is a generalization of ReaderT where the value is not necessarily directly readable through the monad.

Equations

Lake.EquipT ρ m α = (ρ → m α)

Instances For

source

instance Lake.instInhabitedEquipT {ρ : Type u} {m : Type v → Type w} {α : Type v} [Inhabited (m α)] :

Inhabited (Lake.EquipT ρ m α)

Equations

Lake.instInhabitedEquipT = { default := fun (x : ρ) => default }

source

@[inline]

def Lake.EquipT.run {ρ : Type u} {m : Type v → Type w} {α : Type v} (self : Lake.EquipT ρ m α) (r : ρ) :

m α

Equations

self.run r = self r

source

@[inline]

def Lake.EquipT.map {ρ : Type u} {m : Type v → Type w} [Functor m] {α : Type v} {β : Type v} (f : α → β) (self : Lake.EquipT ρ m α) :

Lake.EquipT ρ m β

Equations

Lake.EquipT.map f self fetch = f <$> self fetch

source

instance Lake.EquipT.instFunctor {ρ : Type u} {m : Type v → Type w} [Functor m] :

Functor (Lake.EquipT ρ m)

Equations

Lake.EquipT.instFunctor = { map := fun {α β : Type v} => Lake.EquipT.map, mapConst := fun {α β : Type v} => Lake.EquipT.map ∘ Function.const β }

source

@[inline]

def Lake.EquipT.pure {ρ : Type u} {m : Type v → Type w} [Pure m] {α : Type v} (a : α) :

Lake.EquipT ρ m α

Equations

Lake.EquipT.pure a x = pure a

source

instance Lake.EquipT.instPure {ρ : Type u} {m : Type v → Type w} [Pure m] :

Pure (Lake.EquipT ρ m)

Equations

Lake.EquipT.instPure = { pure := fun {α : Type v} => Lake.EquipT.pure }

source

@[inline]

def Lake.EquipT.compose {ρ : Type u} {m : Type v → Type w} {α₁ : Type v} {α₂ : Type v} {β : Type v} (f : m α₁ → (Unit → m α₂) → m β) (x₁ : Lake.EquipT ρ m α₁) (x₂ : Unit → Lake.EquipT ρ m α₂) :

Lake.EquipT ρ m β

Equations

Lake.EquipT.compose f x₁ x₂ fetch = f (x₁ fetch) fun (x : Unit) => x₂ () fetch

source

@[inline]

def Lake.EquipT.seq {ρ : Type u} {m : Type v → Type w} [Seq m] {α : Type v} {β : Type v} :

Lake.EquipT ρ m (α → β) → (Unit → Lake.EquipT ρ m α) → Lake.EquipT ρ m β

Equations

Lake.EquipT.seq = Lake.EquipT.compose Seq.seq

source

instance Lake.EquipT.instSeq {ρ : Type u} {m : Type v → Type w} [Seq m] :

Seq (Lake.EquipT ρ m)

Equations

Lake.EquipT.instSeq = { seq := fun {α β : Type v} => Lake.EquipT.seq }

source

instance Lake.EquipT.instApplicative {ρ : Type u} {m : Type v → Type w} [Applicative m] :

Applicative (Lake.EquipT ρ m)

Equations

Lake.EquipT.instApplicative = Applicative.mk

source

@[inline]

def Lake.EquipT.bind {ρ : Type u} {m : Type v → Type w} [Bind m] {α : Type v} {β : Type v} (self : Lake.EquipT ρ m α) (f : α → Lake.EquipT ρ m β) :

Lake.EquipT ρ m β

Equations

self.bind f fetch = do let a ← self fetch f a fetch

source

instance Lake.EquipT.instBind {ρ : Type u} {m : Type v → Type w} [Bind m] :

Bind (Lake.EquipT ρ m)

Equations

Lake.EquipT.instBind = { bind := fun {α β : Type v} => Lake.EquipT.bind }

source

instance Lake.EquipT.instMonad {ρ : Type u} {m : Type v → Type w} [Monad m] :

Monad (Lake.EquipT ρ m)

Equations

Lake.EquipT.instMonad = Monad.mk

source

@[inline]

def Lake.EquipT.lift {ρ : Type u} {m : Type v → Type w} {α : Type v} (t : m α) :

Lake.EquipT ρ m α

Equations

Lake.EquipT.lift t x = t

source

instance Lake.EquipT.instMonadLift {ρ : Type u} {m : Type v → Type w} :

MonadLift m (Lake.EquipT ρ m)

Equations

Lake.EquipT.instMonadLift = { monadLift := fun {α : Type v} => Lake.EquipT.lift }

source

instance Lake.EquipT.instMonadFunctor {ρ : Type u} {m : Type v → Type w} :

MonadFunctor m (Lake.EquipT ρ m)

Equations

Lake.EquipT.instMonadFunctor = { monadMap := fun {α : Type v} (f : {β : Type v} → m β → m β) (x : Lake.EquipT ρ m α) (ctx : ρ) => f (x ctx) }

source

@[inline]

def Lake.EquipT.failure {ρ : Type u} {m : Type v → Type w} [Alternative m] {α : Type v} :

Lake.EquipT ρ m α

Equations

Lake.EquipT.failure x = failure

source

@[inline]

def Lake.EquipT.orElse {ρ : Type u} {m : Type v → Type w} [Alternative m] {α : Type v} :

Lake.EquipT ρ m α → (Unit → Lake.EquipT ρ m α) → Lake.EquipT ρ m α

Equations

Lake.EquipT.orElse = Lake.EquipT.compose Alternative.orElse

source

instance Lake.EquipT.instAlternative {ρ : Type u} {m : Type v → Type w} [Alternative m] :

Alternative (Lake.EquipT ρ m)

Equations

Lake.EquipT.instAlternative = Alternative.mk (fun {α : Type v} => Lake.EquipT.failure) fun {α : Type v} => Lake.EquipT.orElse

source

@[inline]

def Lake.EquipT.throw {ρ : Type u} {m : Type v → Type w} {ε : Type v} [MonadExceptOf ε m] {α : Type v} (e : ε) :

Lake.EquipT ρ m α

Equations

Lake.EquipT.throw e x = throw e

source

@[inline]

def Lake.EquipT.tryCatch {ρ : Type u} {m : Type v → Type w} {ε : Type v} [MonadExceptOf ε m] {α : Type v} (self : Lake.EquipT ρ m α) (c : ε → Lake.EquipT ρ m α) :

Lake.EquipT ρ m α

Equations

self.tryCatch c f = tryCatchThe ε (self f) fun (e : ε) => c e f

source

instance Lake.EquipT.instMonadExceptOf {ρ : Type u} {m : Type v → Type w} (ε : Type v) [MonadExceptOf ε m] :

MonadExceptOf ε (Lake.EquipT ρ m)

Equations

Lake.EquipT.instMonadExceptOf ε = { throw := fun {α : Type v} => Lake.EquipT.throw, tryCatch := fun {α : Type v} => Lake.EquipT.tryCatch }

source

@[always_inline]

instance Lake.EquipT.instMonadFinallyOfMonad {ρ : Type u} {m : Type v → Type w} [MonadFinally m] [Monad m] :

MonadFinally (Lake.EquipT ρ m)

Equations

One or more equations did not get rendered due to their size.