Memoizing effectful calls

memoize compute stores the first result of each call in an association list. The underlying computation may be probabilistic or interact with other stateful services. A cache hit does not repeat its effects. The representation is an ordinary list, so later computational realizations can charge for lookup and storage without changing the client program.

Main definitions

• Cslib.memoize: cache one effectful computation per key in a list.

Main results

• Cslib.memoize_repeat: repeated queries share their answer and perform the effect once.
• Cslib.memoize_map: injective key representations and mapped values preserve execution.

References

Adapted from Foundations/Control/Monad/Memoize.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.memoize {Key Value : Type u} {m : Type u → Type v} [Monad m] [BEq Key] (compute : Key → m Value) (key : Key) : StateT (List (Key × Value)) m Value

Cache the result of the first call at each key, sharing the cache through StateT.

theorem Cslib.memoize_of_some {Key Value : Type u} {m : Type u → Type v} [Monad m] [BEq Key] (compute : Key → m Value) (key : Key) (cache : List (Key × Value)) (value : Value) (h : List.lookup key cache = some value) : memoize compute key cache = pure (value, cache)

A previously stored result is returned without repeating the underlying effect.

theorem Cslib.memoize_of_none {Key Value : Type u} {m : Type u → Type v} [Monad m] [BEq Key] (compute : Key → m Value) (key : Key) (cache : List (Key × Value)) (h : List.lookup key cache = none) : memoize compute key cache = do let value ← compute key pure (value, (key, value) :: cache)

A cache miss performs the underlying computation and stores its result.

theorem Cslib.memoize_repeat {Key Value : Type u} {m : Type u → Type v} [Monad m] [BEq Key] [LawfulMonad m] [LawfulBEq Key] (compute : Key → m Value) (key : Key) (cache : List (Key × Value)) : (do let __x ← memoize compute key cache match __x with | (first, cache') => do let __x ← memoize compute key cache' match __x with | (second, cache'') => pure ((first, second), cache'')) = do let __x ← memoize compute key cache match __x with | (value, cache') => pure ((value, value), cache')

Two immediate calls at the same key return the same value and perform the effect once.

theorem Cslib.memoize_map {Key Value : Type u} {m : Type u → Type v} [Monad m] [BEq Key] [LawfulMonad m] [LawfulBEq Key] {Key' Value' : Type u} [BEq Key'] [LawfulBEq Key'] (keyMap : Key ↪ Key') (valueMap : Value → Value') (compute : Key → m Value) (compute' : Key' → m Value') (hcompute : ∀ (key : Key), compute' (keyMap key) = valueMap <$> compute key) (key : Key) (cache : List (Key × Value)) : (fun (result : Value × List (Key × Value)) => (valueMap result.1, List.map (fun (entry : Key × Value) => (keyMap entry.1, valueMap entry.2)) result.2)) <$> memoize compute key cache = memoize compute' (keyMap key) (List.map (fun (entry : Key × Value) => (keyMap entry.1, valueMap entry.2)) cache)

Injectively re-encode cache keys and map stored values. If the samplers commute with the value map, memoization preserves the complete result and re-encoded cache, including duplicates.

theorem Cslib.IsMonadHom.map_memoize {Key Value : Type u} {m : Type u → Type v} [Monad m] [BEq Key] {n : Type u → Type u_1} [Monad n] {f : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => f) (compute : Key → m Value) (key : Key) (cache : List (Key × Value)) : f (memoize compute key cache) = memoize (fun (key : Key) => f (compute key)) key cache

Interpreting the effects commutes with memoization, including its final list cache.