source
class Lake.MonadStore1Of {κ : Type u} (k : κ) (α : semiOutParam (Type v)) (m : Type v → Type w) :
Type (max v w)

A monad equipped with a dependently typed key-value store for a particular key.

- fetch? : m (Option α)
- store : α → m PUnit

Instances

source
class Lake.MonadStore1 {κ : Type u} (k : κ) (α : outParam (Type v)) (m : Type v → Type w) :
Type (max v w)

Similar to `MonadStore1Of`, but `α` is an `outParam` for convenience.

- fetch? : m (Option α)
- store : α → m PUnit

Instances

source
instance Lake.instMonadStore1OfMonadStore1Of {κ✝ : Type u_1} {k : κ✝} {α : Type u_2} {m : Type u_2 → Type u_3} [MonadStore1Of k α m] :
MonadStore1 k α m
Equations

- Lake.instMonadStore1OfMonadStore1Of = { fetch? := Lake.MonadStore1Of.fetch? k, store := Lake.store k }

source
class Lake.MonadDStore (κ : Type u) (β : semiOutParam (κ → Type v)) (m : Type v → Type w) :
Type (max (max u v) w)

A monad equipped with a dependently typed key-object store.

- fetch? (key : κ) : m (Option (β key))
- store (key : κ) : β key → m PUnit

Instances

source
instance Lake.instMonadStore1OfOfMonadDStore {κ : Type u_1} {β : κ → Type u_2} {m : Type u_2 → Type u_3} {k : κ} [MonadDStore κ β m] :
MonadStore1Of k (β k) m
Equations

- Lake.instMonadStore1OfOfMonadDStore = { fetch? := Lake.MonadDStore.fetch? k, store := fun (o : β k) => Lake.MonadDStore.store k o }

source
@[reducible, inline]
abbrev Lake.MonadStore (κ : Type u_1) (α : Type u_2) (m : Type u_2 → Type u_3) :
Type (max (max u_1 u_2) u_3)

A monad equipped with a key-object store.

Equations

- Lake.MonadStore κ α m = Lake.MonadDStore κ (fun (x : κ) => α) m

Instances For

source
instance Lake.instMonadDStoreOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {κ : Type u_4} {β : κ → Type u_1} [MonadLift m n] [MonadDStore κ β m] :
MonadDStore κ β n
Equations

- Lake.instMonadDStoreOfMonadLift = { fetch? := fun (k : κ) => liftM (Lake.fetch? k), store := fun (k : κ) (a : β k) => liftM (Lake.store k a) }

source
@[inline]
def Lake.fetchOrCreate {m : Type u_1 → Type u_2} {κ : Type u_3} {α : Type u_1} [Monad m] (key : κ) [MonadStore1Of key α m] (create : m α) :
m α
Equations

- Lake.fetchOrCreate key create = do let __do_lift ← Lake.fetch? key match __do_lift with | some val => pure val | x => do let val ← create Lake.store key val pure val

Instances For