Source code on Github{-# OPTIONS --cubical-compatible #-}
module Class.Traversable.Core where
open import Class.Prelude
open import Class.Core
open import Class.Functor.Core
open import Class.Applicative.Core
open import Class.Monad.Core
record TraversableA (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
field sequenceA : ⦃ Applicative M ⦄ → F (M A) → M (F A)
traverseA : ⦃ Applicative M ⦄ → (A → M B) → F A → M (F B)
traverseA f = sequenceA ∘ fmap f
open TraversableA ⦃...⦄ public
record Traversable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
field sequence : ⦃ Monad M ⦄ → F (M A) → M (F A)
traverse : ⦃ Monad M ⦄ → (A → M B) → F A → M (F B)
traverse f = sequence ∘ fmap f
open Traversable ⦃...⦄ public