Traversing collections #
This file proves basic properties of traversable and applicative functors and defines
PureTransformation F
, the natural applicative transformation from the identity functor to F
.
References #
Inspired by The Essence of the Iterator Pattern.
The natural applicative transformation from the identity functor
to F
, defined by pure : Π {α}, α → F α
.
Equations
- Traversable.PureTransformation F = { app := @pure F Applicative.toPure, preserves_pure' := ⋯, preserves_seq' := ⋯ }
Instances For
@[simp]
theorem
Traversable.pureTransformation_apply
(F : Type u → Type u)
[Applicative F]
[LawfulApplicative F]
{α : Type u}
(x : id α)
:
(fun {α : Type u} => (Traversable.PureTransformation F).app α) x = pure x
theorem
Traversable.map_eq_traverse_id
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{β : Type u}
{γ : Type u}
(f : β → γ)
:
Functor.map f = traverse (pure ∘ f)
theorem
Traversable.map_traverse
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{F : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
{α : Type u}
{β : Type u}
{γ : 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]
[LawfulTraversable t]
{F : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
{α : Type u}
{β : Type u}
{γ : Type u}
(f : β → F γ)
(g : α → β)
(x : t α)
:
theorem
Traversable.pure_traverse
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{F : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
{α : Type u}
(x : t α)
:
theorem
Traversable.id_sequence
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{α : Type u}
(x : t α)
:
theorem
Traversable.comp_sequence
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{F : Type u → Type u}
{G : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
[Applicative G]
[LawfulApplicative G]
{α : Type u}
(x : t (F (G α)))
:
theorem
Traversable.naturality'
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{F : Type u → Type u}
{G : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
[Applicative G]
[LawfulApplicative G]
{α : Type u}
(η : ApplicativeTransformation F G)
(x : t (F α))
:
theorem
Traversable.traverse_id
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{α : Type u}
:
theorem
Traversable.traverse_comp
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{F : Type u → Type u}
{G : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
[Applicative G]
[LawfulApplicative G]
{α : Type u}
{β : Type u}
{γ : 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]
[LawfulTraversable t]
{β : Type u}
{γ : Type u}
(f : β → γ)
:
traverse (pure ∘ f) = pure ∘ Functor.map f
theorem
Traversable.traverse_map'
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{G : Type u → Type u}
[Applicative G]
[LawfulApplicative G]
{α : Type u}
{β : Type u}
{γ : Type u}
(g : α → β)
(h : β → G γ)
:
theorem
Traversable.map_traverse'
{t : Type u → Type u}
[Traversable t]
[LawfulTraversable t]
{G : Type u → Type u}
[Applicative G]
[LawfulApplicative G]
{α : Type u}
{β : Type u}
{γ : 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]
[LawfulTraversable t]
{F : Type u → Type u}
{G : Type u → Type u}
[Applicative F]
[LawfulApplicative F]
[Applicative G]
[LawfulApplicative G]
{α : Type u}
{β : Type u}
(η : ApplicativeTransformation F G)
(f : α → F β)
: