mathlib3 documentation

control.traversable.basic

Traversable type class #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Type classes for traversing collections. The concepts and laws are taken from http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Traversable.html

Traversable collections are a generalization of functors. Whereas functors (such as list) allow us to apply a function to every element, it does not allow functions which external effects encoded in a monad. Consider for instance a functor invite : email → io response that takes an email address, sends an email and waits for a response. If we have a list guests : list email, using calling invite using map gives us the following: map invite guests : list (io response). It is not what we need. We need something of type io (list response). Instead of using map, we can use traverse to send all the invites: traverse invite guests : io (list response). traverse applies invite to every element of guests and combines all the resulting effects. In the example, the effect is encoded in the monad io but any applicative functor is accepted by traverse.

For more on how to use traversable, consider the Haskell tutorial: https://en.wikibooks.org/wiki/Haskell/Traversable

Main definitions #

traversable type class - exposes the traverse function
sequence - based on traverse, turns a collection of effects into an effect returning a collection
is_lawful_traversable - laws for a traversable functor
applicative_transformation - the notion of a natural transformation for applicative functors

Tags #

traversable iterator functor applicative

References #

"Applicative Programming with Effects", by Conor McBride and Ross Paterson, Journal of Functional Programming 18:1 (2008) 1-13, online at http://www.soi.city.ac.uk/~ross/papers/Applicative.html
"The Essence of the Iterator Pattern", by Jeremy Gibbons and Bruno Oliveira, in Mathematically-Structured Functional Programming, 2006, online at http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/#iterator
"An Investigation of the Laws of Traversals", by Mauro Jaskelioff and Ondrej Rypacek, in Mathematically-Structured Functional Programming, 2012, online at http://arxiv.org/pdf/1202.2919

structure applicative_transformation (F : Type u → Type v) [applicative F] [is_lawful_applicative F] (G : Type u → Type w) [applicative G] [is_lawful_applicative G] :

Type (max (u+1) v w)

app : Π (α : Type ?), F α → G α
preserves_pure' : ∀ {α : Type ?} (x : α), self.app α (has_pure.pure x) = has_pure.pure x
preserves_seq' : ∀ {α β : Type ?} (x : F (α → β)) (y : F α), self.app β (x <*> y) = self.app (α → β) x <*> self.app α y

A transformation between applicative functors. It is a natural transformation such that app preserves the has_pure.pure and functor.map (<*>) operations. See applicative_transformation.preserves_map for naturality.

Instances for applicative_transformation

applicative_transformation.has_sizeof_inst
applicative_transformation.has_coe_to_fun
applicative_transformation.inhabited

@[protected, instance]

def applicative_transformation.has_coe_to_fun (F : Type u → Type v) [applicative F] [is_lawful_applicative F] (G : Type u → Type w) [applicative G] [is_lawful_applicative G] :

has_coe_to_fun (applicative_transformation F G) (λ (_x : applicative_transformation F G), Π {α : Type u}, F α → G α)

Equations

applicative_transformation.has_coe_to_fun F G = {coe := applicative_transformation.app _inst_4}

@[simp]

theorem applicative_transformation.app_eq_coe {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) :

η.app = ⇑η

@[simp]

theorem applicative_transformation.coe_mk {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (f : Π (α : Type u), F α → G α) (pp : ∀ {α : Type u} (x : α), f α (has_pure.pure x) = has_pure.pure x) (ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f β (x <*> y) = f (α → β) x <*> f α y) :

⇑{app := f, preserves_pure' := pp, preserves_seq' := ps} = f

@[protected]

theorem applicative_transformation.congr_fun {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η η' : applicative_transformation F G) (h : η = η') {α : Type u} (x : F α) :

⇑η x = ⇑η' x

@[protected]

theorem applicative_transformation.congr_arg {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u} {x y : F α} (h : x = y) :

⇑η x = ⇑η y

theorem applicative_transformation.coe_inj {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] ⦃η η' : applicative_transformation F G⦄ (h : ⇑η = ⇑η') :

η = η'

@[ext]

theorem applicative_transformation.ext {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] ⦃η η' : applicative_transformation F G⦄ (h : ∀ (α : Type u) (x : F α), ⇑η x = ⇑η' x) :

η = η'

theorem applicative_transformation.ext_iff {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] {η η' : applicative_transformation F G} :

η = η' ↔ ∀ (α : Type u) (x : F α), ⇑η x = ⇑η' x

theorem applicative_transformation.preserves_pure {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u} (x : α) :

⇑η (has_pure.pure x) = has_pure.pure x

theorem applicative_transformation.preserves_seq {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (x : F (α → β)) (y : F α) :

⇑η (x <*> y) = ⇑η x <*> ⇑η y

theorem applicative_transformation.preserves_map {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (x : α → β) (y : F α) :

⇑η (x <$> y) = x <$> ⇑η y

theorem applicative_transformation.preserves_map' {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (x : α → β) :

⇑η ∘ functor.map x = functor.map x ∘ ⇑η

def applicative_transformation.id_transformation {F : Type u → Type v} [applicative F] [is_lawful_applicative F] :

applicative_transformation F F

The identity applicative transformation from an applicative functor to itself.

Equations

applicative_transformation.id_transformation = {app := λ (α : Type u), id, preserves_pure' := _, preserves_seq' := _}

@[protected, instance]

def applicative_transformation.inhabited {F : Type u → Type v} [applicative F] [is_lawful_applicative F] :

inhabited (applicative_transformation F F)

Equations

applicative_transformation.inhabited = {default := applicative_transformation.id_transformation _inst_2}

def applicative_transformation.comp {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] {H : Type u → Type s} [applicative H] [is_lawful_applicative H] (η' : applicative_transformation G H) (η : applicative_transformation F G) :

applicative_transformation F H

The composition of applicative transformations.

Equations

η'.comp η = {app := λ (α : Type u) (x : F α), ⇑η' (⇑η x), preserves_pure' := _, preserves_seq' := _}

@[simp]

theorem applicative_transformation.comp_apply {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] {H : Type u → Type s} [applicative H] [is_lawful_applicative H] (η' : applicative_transformation G H) (η : applicative_transformation F G) {α : Type u} (x : F α) :

⇑(η'.comp η) x = ⇑η' (⇑η x)

theorem applicative_transformation.comp_assoc {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] {H : Type u → Type s} [applicative H] [is_lawful_applicative H] {I : Type u → Type t} [applicative I] [is_lawful_applicative I] (η'' : applicative_transformation H I) (η' : applicative_transformation G H) (η : applicative_transformation F G) :

(η''.comp η').comp η = η''.comp (η'.comp η)

@[simp]

theorem applicative_transformation.comp_id {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) :

η.comp applicative_transformation.id_transformation = η

@[simp]

theorem applicative_transformation.id_comp {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {G : Type u → Type w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) :

applicative_transformation.id_transformation.comp η = η

@[class]

structure traversable (t : Type u → Type u) :

Type (u+1)

to_functor : functor t
traverse : Π {m : Type ? → Type ?} [_inst_1 : applicative m] {α β : Type ?}, (α → m β) → t α → m (t β)

A traversable functor is a functor along with a way to commute with all applicative functors (see sequence). For example, if t is the traversable functor list and m is the applicative functor io, then given a function f : α → io β, the function functor.map f is list α → list (io β), but traverse f is list α → io (list β).

Instances of this typeclass

Instances of other typeclasses for traversable

traversable.has_sizeof_inst

def sequence {t : Type u → Type u} {α : Type u} {f : Type u → Type u} [applicative f] [traversable t] :

t (f α) → f (t α)

A traversable functor commutes with all applicative functors.

Equations

sequence = traversable.traverse id

@[class]

structure is_lawful_traversable (t : Type u → Type u) [traversable t] :

Type (u+1)

to_is_lawful_functor : is_lawful_functor t
id_traverse : ∀ {α : Type ?} (x : t α), traversable.traverse id.mk x = x
comp_traverse : ∀ {F G : Type ? → Type ?} [_inst_1_1 : applicative F] [_inst_2 : applicative G] [_inst_3 : is_lawful_applicative F] [_inst_4 : is_lawful_applicative G] {α β γ : Type ?} (f : β → F γ) (g : α → G β) (x : t α), traversable.traverse (functor.comp.mk ∘ functor.map f ∘ g) x = functor.comp.mk (traversable.traverse f <$> traversable.traverse g x)
traverse_eq_map_id : ∀ {α β : Type ?} (f : α → β) (x : t α), traversable.traverse (id.mk ∘ f) x = id.mk (f <$> x)
naturality : ∀ {F G : Type ? → Type ?} [_inst_1_1 : applicative F] [_inst_2 : applicative G] [_inst_3 : is_lawful_applicative F] [_inst_4 : is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type ?} (f : α → F β) (x : t α), ⇑η (traversable.traverse f x) = traversable.traverse (⇑η ∘ f) x

A traversable functor is lawful if its traverse satisfies a number of additional properties. It must send id.mk to id.mk, send the composition of applicative functors to the composition of the traverse of each, send each function f to λ x, f <$> x, and satisfy a naturality condition with respect to applicative transformations.

Instances of this typeclass

Instances of other typeclasses for is_lawful_traversable

is_lawful_traversable.has_sizeof_inst

@[protected, instance]

def id.traversable :

Equations

id.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := λ (_x : Type u_1 → Type u_1) (_x_1 : applicative _x) (_x_1 _x_2 : Type u_1), id}

@[protected, instance]

def id.is_lawful_traversable :

is_lawful_traversable id

Equations

id.is_lawful_traversable = {to_is_lawful_functor := id.is_lawful_traversable._proof_1, id_traverse := id.is_lawful_traversable._proof_2, comp_traverse := id.is_lawful_traversable._proof_3, traverse_eq_map_id := id.is_lawful_traversable._proof_4, naturality := id.is_lawful_traversable._proof_5}

@[protected, instance]

def option.traversable :

traversable option

Equations

option.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := option.traverse}

@[protected, instance]

def list.traversable :

traversable list

Equations

list.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := list.traverse}

@[protected]

def sum.traverse {σ : Type u} {F : Type u → Type u} [applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :

σ ⊕ α → F (σ ⊕ β)

Defines a traverse function on the second component of a sum type. This is used to give a traversable instance for the functor σ ⊕ -.

Equations

sum.traverse f (sum.inr x) = sum.inr <$> f x
sum.traverse f (sum.inl x) = has_pure.pure (sum.inl x)

@[protected, instance]

def sum.traversable {σ : Type u} :

traversable (sum σ)

Equations

sum.traversable = {to_functor := applicative.to_functor monad.to_applicative, traverse := sum.traverse σ}