Control.Comonad.Transformerless.Store

newtype Store s a

Constructors

• Store (Tuple (s -> a) s)

Instances

• Newtype (Store s a) _
• Functor (Store s)
• Extend (Store s)

  Law: extend f <<< extend g = extend (f <<< extend g) Proof: RHS := extend (\ x -> f (extend g x)) y = extend (\ x -> f (extend g (sx, s))) (s'y, s') = extend (\ x -> f (\ t -> g (sx, s), s)) (s'y, s') = (\ t' -> (\ x -> f (\ t -> g (sx, s), s)) (s'y, s'), s') LHS := (extend f <<< extend g) y = extend f (extend g y) = extend f (extend g (sy, s)) = extend f (\ s' -> g (sy, s), s) = (\ t -> f (\ s' -> g (sy, s), s) , s) = TODO: finish this

• Comonad (Store s)

runStore :: forall a s. Store s a -> Tuple (s -> a) s

store :: forall a s. Tuple (s -> a) s -> Store s a

peek :: forall a s. s -> Store s a -> a

Law: peek (pos x) x = extract x Proof: RHS := extract (f, s) = f s LHS := peek (pos (f, s)) (f, s) = peek s (f, s) = peek s (f, _) = f s

pos :: forall a s. Store s a -> s

Law: pos (extend _ x) = pos x Proof: RHS := pos (, s) LHS := pos (extend (f, s)) = pos (extend _ (, s)) = pos (, s)