module Stdlib.Trait.Traversable.Polymorphic;

import Stdlib.Function open;
import Stdlib.Trait.Functor.Polymorphic open;
import Stdlib.Trait.Applicative open;

--- A trait for traversing a structure while performing applicative effects
trait
type Traversable (T : Type -> Type) :=
  mkTraversable@{
    {{functorI}} : Functor T;
    traverse
      : {F : Type -> Type}
        -> {{Applicative F}}
        -> {A B : Type}
        -> (A -> F B)
        -> T A
        -> F (T B);
    sequenceA
      : {F : Type -> Type}
        -> {{Applicative F}}
        -> {A : Type}
        -> T (F A)
        -> F (T A);
  };

open Traversable public;

-- Default implementation of sequenceA using traverse
{-# inline: true #-}
defaultSequenceA
  {T : Type -> Type}
  {F : Type -> Type}
  {{Applicative F}}
  {A : Type}
  (trav : {F : Type -> Type}
    -> {{Applicative F}}
    -> {A B : Type}
    -> (A -> F B)
    -> T A
    -> F (T B))
  (tfa : T (F A))
  : F (T A) := trav id tfa;

-- Default implementation of traverse using sequenceA
{-# inline: true #-}
defaultTraverse
  {T : Type -> Type}
  {{Functor T}}
  {F : Type -> Type}
  {{Applicative F}}
  {A B : Type}
  (seqA : {F : Type -> Type}
    -> {{Applicative F}}
    -> {A : Type}
    -> T (F A)
    -> F (T A))
  (f : A -> F B)
  (ta : T A)
  : F (T B) := seqA (map f ta);