Traversing collections #
This file proves basic properties of traversable and applicative functors and defines
pure_transformation F, the natural applicative transformation from the identity functor to F.
References #
Inspired by The Essence of the Iterator Pattern.
def
traversable.pure_transformation
(F : Type u → Type u)
[applicative F]
[is_lawful_applicative F] :
The natural applicative transformation from the identity functor
to F, defined by pure : Π {α}, α → F α.
Equations
- traversable.pure_transformation F = {app := pure applicative.to_has_pure, preserves_pure' := _, preserves_seq' := _}
@[simp]
theorem
traversable.pure_transformation_apply
(F : Type u → Type u)
[applicative F]
[is_lawful_applicative F]
{α : Type u}
(x : id α) :
⇑(traversable.pure_transformation F) x = pure x
theorem
traversable.map_eq_traverse_id
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{β γ : Type u}
(f : β → γ) :
functor.map f = traverse (id.mk ∘ f)
theorem
traversable.map_traverse
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α β γ : Type u}
(g : α → F β)
(f : β → γ)
(x : t α) :
functor.map f <$> traverse g x = traverse (functor.map f ∘ g) x
theorem
traversable.traverse_map
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α β γ : Type u}
(f : β → F γ)
(g : α → β)
(x : t α) :
theorem
traversable.pure_traverse
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α : Type u}
(x : t α) :
theorem
traversable.id_sequence
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{α : Type u}
(x : t α) :
theorem
traversable.comp_sequence
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α : Type u}
(x : t (F (G α))) :
theorem
traversable.naturality'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α : Type u}
(η : applicative_transformation F G)
(x : t (F α)) :
theorem
traversable.traverse_id
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{α : Type u} :
theorem
traversable.traverse_comp
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α β γ : Type u}
(g : α → F β)
(h : β → G γ) :
traverse (functor.comp.mk ∘ functor.map h ∘ g) = functor.comp.mk ∘ functor.map (traverse h) ∘ traverse g
theorem
traversable.traverse_eq_map_id'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{β γ : Type u}
(f : β → γ) :
theorem
traversable.traverse_map'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{G : Type u → Type u}
[applicative G]
[is_lawful_applicative G]
{α β γ : Type u}
(g : α → β)
(h : β → G γ) :
theorem
traversable.map_traverse'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{G : Type u → Type u}
[applicative G]
[is_lawful_applicative G]
{α β γ : Type u}
(g : α → G β)
(h : β → γ) :
traverse (functor.map h ∘ g) = functor.map (functor.map h) ∘ traverse g
theorem
traversable.naturality_pf
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α β : Type u}
(η : applicative_transformation F G)
(f : α → F β) :