Skip to content

Instantly share code, notes, and snippets.

@aljce

aljce/Trav.agda

Created August 3, 2022 20:53
Show Gist options
  • Save aljce/907982b002e299590a37c49b90131f15 to your computer and use it in GitHub Desktop.
Save aljce/907982b002e299590a37c49b90131f15 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment