Traversable type class

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
• LawfulTraversable - laws for a traversable functor
• ApplicativeTransformation - 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 ApplicativeTransformation (F : Type u → Type v) [Applicative F] (G : Type u → Type w) [Applicative G] : Type (max (u + 1) v w)

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

• app : (α : Type u) → F α → G α

  The function on objects defined by an ApplicativeTransformation.

• preserves_pure' : ∀ {α : Type u} (x : α), self.app α (pure x) = pure x

  An ApplicativeTransformation preserves pure.

• preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), self.app β (x <*> y) = self.app (α → β) x <*> self.app α y

  An ApplicativeTransformation intertwines seq.

theorem ApplicativeTransformation.preserves_pure' {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (self : ApplicativeTransformation F G) {α : Type u} (x : α) : self.app α (pure x) = pure x

An ApplicativeTransformation preserves pure.

theorem ApplicativeTransformation.preserves_seq' {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (self : ApplicativeTransformation F G) {α : Type u} {β : Type u} (x : F (α → β)) (y : F α) : self.app β (x <*> y) = self.app (α → β) x <*> self.app α y

An ApplicativeTransformation intertwines seq.

instance ApplicativeTransformation.instCoeFunForallForall (F : Type u → Type v) [Applicative F] (G : Type u → Type w) [Applicative G] : CoeFun (ApplicativeTransformation F G) fun (x : ApplicativeTransformation F G) => {α : Type u} → F α → G α

Equations

• ApplicativeTransformation.instCoeFunForallForall F G = { coe := fun (η : ApplicativeTransformation F G) {α : Type ?u.38} => η.app α }

theorem ApplicativeTransformation.app_eq_coe {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) : η.app = fun {α : Type u} => η.app α

@[simp]

theorem ApplicativeTransformation.coe_mk {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (f : (α : Type u) → F α → G α) (pp : ∀ {α : Type u} (x : α), f α (pure x) = pure x) (ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f β (x <*> y) = f (α → β) x <*> f α y) : (fun {α : Type u} => { app := f, preserves_pure' := pp, preserves_seq' := ps }.app α) = f

theorem ApplicativeTransformation.congr_fun {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) (η' : ApplicativeTransformation F G) (h : η = η') {α : Type u} (x : F α) : (fun {α : Type u} => η.app α) x = (fun {α : Type u} => η'.app α) x

theorem ApplicativeTransformation.congr_arg {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) {α : Type u} {x : F α} {y : F α} (h : x = y) : (fun {α : Type u} => η.app α) x = (fun {α : Type u} => η.app α) y

theorem ApplicativeTransformation.coe_inj {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] ⦃η : ApplicativeTransformation F G⦄ ⦃η' : ApplicativeTransformation F G⦄ (h : (fun {α : Type u} => η.app α) = fun {α : Type u} => η'.app α) : η = η'

theorem ApplicativeTransformation.ext {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] ⦃η : ApplicativeTransformation F G⦄ ⦃η' : ApplicativeTransformation F G⦄ (h : ∀ (α : Type u) (x : F α), (fun {α : Type u} => η.app α) x = (fun {α : Type u} => η'.app α) x) : η = η'

theorem ApplicativeTransformation.preserves_pure {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) {α : Type u} (x : α) : (fun {α : Type u} => η.app α) (pure x) = pure x

theorem ApplicativeTransformation.preserves_seq {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) {α : Type u} {β : Type u} (x : F (α → β)) (y : F α) : (fun {α : Type u} => η.app α) (x <*> y) = (fun {α : Type u} => η.app α) x <*> (fun {α : Type u} => η.app α) y

theorem ApplicativeTransformation.preserves_map {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α : Type u} {β : Type u} (x : α → β) (y : F α) : (fun {α : Type u} => η.app α) (x <$> y) = x <$> (fun {α : Type u} => η.app α) y

theorem ApplicativeTransformation.preserves_map' {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α : Type u} {β : Type u} (x : α → β) : (fun {α : Type u} => η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α : Type u} => η.app α

def ApplicativeTransformation.idTransformation {F : Type u → Type v} [Applicative F] : ApplicativeTransformation F F

The identity applicative transformation from an applicative functor to itself.

Equations

• ApplicativeTransformation.idTransformation = { app := fun (x : Type ?u.18) => id, preserves_pure' := ⋯, preserves_seq' := ⋯ }

instance ApplicativeTransformation.instInhabited {F : Type u → Type v} [Applicative F] : Inhabited (ApplicativeTransformation F F)

Equations

• ApplicativeTransformation.instInhabited = { default := ApplicativeTransformation.idTransformation }

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

The composition of applicative transformations.

Equations

• η'.comp η = { app := fun (x : Type ?u.55) (x_1 : F x) => (fun {α : Type ?u.55} => η'.app α) ((fun {α : Type ?u.55} => η.app α) x_1), preserves_pure' := ⋯, preserves_seq' := ⋯ }

@[simp]

theorem ApplicativeTransformation.comp_apply {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] {H : Type u → Type s} [Applicative H] (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) {α : Type u} (x : F α) : (fun {α : Type u} => (η'.comp η).app α) x = (fun {α : Type u} => η'.app α) ((fun {α : Type u} => η.app α) x)

theorem ApplicativeTransformation.comp_assoc {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] {H : Type u → Type s} [Applicative H] {I : Type u → Type t} [Applicative I] (η'' : ApplicativeTransformation H I) (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) : (η''.comp η').comp η = η''.comp (η'.comp η)

@[simp]

theorem ApplicativeTransformation.comp_id {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) : η.comp ApplicativeTransformation.idTransformation = η

@[simp]

theorem ApplicativeTransformation.id_comp {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) : ApplicativeTransformation.idTransformation.comp η = η

class Traversable (t : Type u → Type u) extends Functor : Type (u + 1)

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 β).

• map : {α β : Type u} → (α → β) → t α → t β
• mapConst : {α β : Type u} → α → t β → t α
• traverse : {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → t α → m (t β)

  The function commuting a traversable functor t with an arbitrary applicative functor m.

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 = traverse id

class LawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor : Prop

A traversable functor is lawful if its traverse satisfies a number of additional properties. It must send pure : α → Id α to pure, send the composition of applicative functors to the composition of the traverse of each, send each function f to fun x ↦ f <$> x, and satisfy a naturality condition with respect to applicative transformations.

• map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
• id_map : ∀ {α : Type u} (x : t α), id <$> x = x
• comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : t α), (h ∘ g) <$> x = h <$> g <$> x
• id_traverse : ∀ {α : Type u} (x : t α), traverse pure x = x

  traverse plays well with pure of the identity monad

• comp_traverse : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α), traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)

  traverse plays well with composition of applicative functors.

• traverse_eq_map_id : ∀ {α β : Type u} (f : α → β) (x : t α), traverse (pure ∘ f) x = id.mk (f <$> x)

  An axiom for traverse involving pure : β → Id β.

• naturality : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α), (fun {α : Type u} => η.app α) (traverse f x) = traverse ((fun {α : Type u} => η.app α) ∘ f) x

  The naturality axiom explaining how lawful traversable functors should play with lawful applicative functors.

theorem LawfulTraversable.id_traverse {t : Type u → Type u} : ∀ {inst : Traversable t} [self : LawfulTraversable t] {α : Type u} (x : t α), traverse pure x = x

traverse plays well with pure of the identity monad

theorem LawfulTraversable.comp_traverse {t : Type u → Type u} : ∀ {inst : Traversable t} [self : LawfulTraversable t] {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [inst_3 : LawfulApplicative F] [inst_4 : LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α), traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)

traverse plays well with composition of applicative functors.

theorem LawfulTraversable.traverse_eq_map_id {t : Type u → Type u} : ∀ {inst : Traversable t} [self : LawfulTraversable t] {α β : Type u} (f : α → β) (x : t α), traverse (pure ∘ f) x = id.mk (f <$> x)

An axiom for traverse involving pure : β → Id β.

theorem LawfulTraversable.naturality {t : Type u → Type u} : ∀ {inst : Traversable t} [self : LawfulTraversable t] {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [inst_3 : LawfulApplicative F] [inst_4 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α), (fun {α : Type u} => η.app α) (traverse f x) = traverse ((fun {α : Type u} => η.app α) ∘ f) x

The naturality axiom explaining how lawful traversable functors should play with lawful applicative functors.

instance instTraversableId : Traversable Id

Equations

• instTraversableId = Traversable.mk fun {m : Type ?u.10 → Type ?u.10} [Applicative m] {α β : Type ?u.10} => id

instance instLawfulTraversableId : LawfulTraversable Id

Equations

• instLawfulTraversableId = ⋯

instance instTraversableOption : Traversable Option

Equations

• instTraversableOption = Traversable.mk fun {m : Type ?u.9 → Type ?u.9} [Applicative m] {α β : Type ?u.9} => Option.traverse

instance instTraversableList : Traversable List

Equations

• instTraversableList = Traversable.mk fun {m : Type ?u.9 → Type ?u.9} [Applicative m] {α β : Type ?u.9} => List.traverse

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.inl x_1) = pure (Sum.inl x_1)
• Sum.traverse f (Sum.inr x_1) = Sum.inr <$> f x_1

instance instTraversableSum {σ : Type u} : Traversable (Sum σ)

Equations

• instTraversableSum = Traversable.mk (@Sum.traverse σ)