Trav.agda

module Para where

open Agda.Primitive using (lsuc)

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

infixr 5 _∷_
data Vec {ℓ} : ℕ → Set ℓ → Set ℓ where
  [] : ∀ {A : Set ℓ} → Vec zero A
  _∷_ : ∀ {n} {A : Set ℓ} → A → Vec n A → Vec (suc n) A

module _ {ℓ} (F : Set ℓ → Set ℓ) where
  record Functor : Set (lsuc ℓ) where
    field
      map : ∀ {A B : Set ℓ} → (A → B) → F A → F B
  open Functor {{...}} public

  record Applicative : Set (lsuc ℓ) where
    infixl 4 _<*>_
    field
      pure : ∀ {A : Set ℓ} → A → F A
      _<*>_ : ∀ {A B : Set ℓ} → F (A → B) → F A → F B
  open Applicative {{...}} public

module _ {ℓ} (T : Set ℓ → Set ℓ) where
  record Traversable : Set (lsuc ℓ) where
    field
      traverse : ∀ {F : Set ℓ → Set ℓ} {{appF : Applicative F}} {A B : Set ℓ} → (A → F B) → T A → F (T B)
open Traversable {{...}} public

instance
  VecTraversable : ∀ {ℓ} {n} → Traversable {ℓ} (Vec n)
  VecTraversable {ℓ} {n} = record { traverse = vecTraverse }
    where
      module _ {F : Set ℓ → Set ℓ} {{appF : Applicative F}} where
        vecTraverse : ∀ {m} {A B : Set ℓ} → (A → F B) → Vec m A → F (Vec m B)
        vecTraverse f [] = pure []
        vecTraverse f (x ∷ xs) = pure _∷_ <*> f x <*> vecTraverse f xs

module Goals {ℓ} {A : Set ℓ} where
  idᵥ : ∀ {n} {m} → Vec m (Vec n A) → Vec m (Vec n A)
  idᵥ = traverse {!!}
  transpose : ∀ {n m} → Vec n (Vec m A) → Vec m (Vec n A)
  transpose = traverse {!!}
open Goals public

ex-vec : Vec 3 (Vec 3 ℕ)
ex-vec = (1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ (7 ∷ 8 ∷ 9 ∷ []) ∷ []

example1 : Vec 3 (Vec 3 ℕ)
example1 = transpose ex-vec