TraversableVec.agda

module TraversableVec where

id : forall {k}{X : Set k} -> X -> X
id x = x

_o_ : forall {i j k}
      {A : Set i}{B : A -> Set j}{C : (a : A) -> B a -> Set k} ->
      (f : {a : A}(b : B a) -> C a b) ->
      (g : (a : A) -> B a) ->
      (a : A) -> C a (g a)
f o g = \ a -> f (g a)
infixl 2 _o_

data Nat : Set where
  zero  :         Nat
  suc   : Nat ->  Nat

{-# BUILTIN NATURAL Nat #-}

data Vec (X : Set) : Nat -> Set where
  <>   :                               Vec X zero
  _,_  : {n : Nat} -> X -> Vec X n ->  Vec X (suc n)

record Applicative (F : Set -> Set) : Set1 where
  infixl 2 _<*>_
  field
    pure    : forall {X} -> X -> F X
    _<*>_   : forall {S T} -> F (S -> T) -> F S -> F T
open Applicative {{...}} public

instance
  applicativeId : Applicative id
  applicativeId = record
    { pure = id
    ; _<*>_ = \ f x -> f x
    }

  applicativeComp : forall {F G} -> Applicative F -> Applicative G -> Applicative (F o G)
  applicativeComp aF aG = record
    { pure = AF.pure o AG.pure
    ; _<*>_ = \ fgf fgs -> (AF.pure AG._<*>_) AF.<*> fgf AF.<*> fgs
    } where
      module AG = Applicative aG
      module AF = Applicative aF

record Traversable (F : Set -> Set) : Set1 where
  field
    traverse :  forall {G S T}{{AG : Applicative G}} ->
                (S -> G T) -> F S -> G (F T)
open Traversable {{...}} public

instance
  traversableVec : {n : Nat} -> Traversable \ X -> Vec X n
  traversableVec = record { traverse = vtr } where
    vtr :  forall {n G S T}{{_ : Applicative G}} ->
           (S -> G T) -> Vec S n -> G (Vec T n)
    vtr {{aG}} f <>        = pure {{aG}} <>
    vtr {{aG}} f (s , ss)  = pure {{aG}} _,_ AG.<*> f s AG.<*> vtr f ss
      where
      module AG = Applicative aG