Traversable.agda


module Haskell.Prim.Traversable where

open import Haskell.Prim
open import Haskell.Prim.Applicative
open import Haskell.Prim.Functor
open import Haskell.Prim.Foldable
open import Haskell.Prim.Monad
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either
open import Haskell.Prim.Tuple

--------------------------------------------------
-- Traversable

-- ** base
record Traversable (t : Type → Type) : Type₁ where
  field
    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
    overlap ⦃ functor ⦄ : Functor t
    overlap ⦃ foldable ⦄ : Foldable t

    sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
    mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
    sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
-- ** defaults
record DefaultTraversable (t : Type → Type) : Type₁ where
  field
    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
    overlap ⦃ functor ⦄ : Functor t
    overlap ⦃ foldable ⦄ : Foldable t

  sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
  sequenceA = traverse id

  mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
  mapM = traverse

  sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
  sequence = sequenceA
-- ** export
open Traversable ⦃...⦄ public
{-# COMPILE AGDA2HS Traversable existing-class #-}
-- ** instances
private
  mkTraversable : DefaultTraversable t → Traversable t
  mkTraversable x = record {DefaultTraversable x}

  infix 0 traverse=_
  traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄
            → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b))
            → Traversable t
  traverse= x = record {DefaultTraversable (record {traverse = x})}
instance
  open DefaultTraversable

  iTraversableList : Traversable List
  iTraversableList = traverse= traverseList
    where
      traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b)
      traverseList f []       = pure []
      traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈

  iTraversableMaybe : Traversable Maybe
  iTraversableMaybe = traverse= λ where
    f Nothing  → pure Nothing
    f (Just x) → Just <$> f x

  iTraversableEither : Traversable (Either a)
  iTraversableEither = traverse= λ where
    f (Left  x) → pure (Left x)
    f (Right y) → Right <$> f y

  iTraversablePair : Traversable (a ×_)
  iTraversablePair = traverse= λ
    f (x , y) → (x ,_) <$> f y