MoA

content.lagda.md

\tableofcontents

Intro

Imports

{-# OPTIONS --with-K --exact-split #-}
module content where

open import Data.Vec
  hiding ( take ; drop )

open import Data.Nat
open import Data.Nat.Properties 
open import Data.Product
import Data.Fin


import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

Machinery

$$ a = ⟨2 3 ⟩ [1, 2, 3, 4, 5, 6] $$

\begin{align*} ⟨5, 6 ⟩ &: \mathsf{shape}(2)\ ⟨6,7,4 ⟩ &: \mathsf{shape}(3) \end{align*}

module MoA where
  variable
    E : Set

Vectors

  take-vec : ∀ {l}{A : Set}
    → (n : ℕ)
    → (v : Vec A l)
    → (p : n ≤ l)
    → Vec A n
  take-vec zero _ _ = []
  take-vec (suc n) (x ∷ xs) (s≤s p) = x ∷ take-vec n xs p

  drop-vec : ∀ {l : ℕ}{A : Set}
    → (n : ℕ)
    → (v : Vec A l)
    → (p : n ≤ l)
    → Vec A (l - n)
  drop-vec zero v _ = v
  drop-vec (suc n) (x ∷ xs) (s≤s p) = drop-vec n xs p

Shapes

  Shape : ℕ → Set
  Shape = Vec ℕ

  take-shape : ∀ {d}
    → (n : ℕ)
    → (s : Shape (1 + d)) 
    → (p : n ≤ head s)
    → Shape (1 + d)
  take-shape n s  p = n ∷ tail s

  drop-shape : ∀ {d}
    → (n : ℕ)
    → (s : Shape (1 + d)) 
    → (p : n ≤ head s)
    → Shape (1 + d)
  drop-shape zero s p = s
  drop-shape (suc n) (x ∷ xs) p
    = drop-shape n (x ∷ xs) (≤-trans (n≤1+n n) p)

  ∏ : ∀ {d} → Shape d → ℕ
  ∏  s = foldr _ _*_ 1 s

  ex1 = 5 ∷ 6 ∷ [] 
  ex2 = 6 ∷ 7 ∷ 4 ∷ [] 

Arrays

  module Arrays (A : Set) where

    record Array {d : ℕ} (s : Shape d) : Set
      where
      constructor mkarr
      field 
        vec : Vec A (∏ s)

    dim : ∀ {d}{s} → Array {d} s → ℕ
    dim {d = d} _ = d

    ρ : ∀ {d}{s} → Array {d} s → Shape d
    ρ {s = s} _ = s
    
    elems : ∀ {d}{s} → Array {d} s → Vec A (∏ s)
    elems a = Array.vec a

    shape-elim
      : ∀ {d : ℕ}
      → (P : Shape d → Set)
      → ((p : 0 ≡ d) → P (subst Shape p []) )
      → (∀ {n} e s  → (p : (1 + n ≡ d)) →  P (subst Shape p (e ∷ s)))
      → (∀ s → P s)
    shape-elim P base-case cons-case []      = base-case refl
    shape-elim P base-case cons-case (x ∷ s) = cons-case x s refl

    pi-hd-tl 
      : ∀ {d : ℕ} (s : Shape (1 + d))
      → ∏ s ≡ ((head s) * ∏ (tail s))
    pi-hd-tl (x ∷ xs) = refl

    reshape
      : ∀ {d₁ d₂ : ℕ} {s₁ : Shape d₁}
      → (a : Array s₁) 
      → (s₂ : Shape d₂)
      → (p : ∏ s₁ ≡ ∏ s₂)
      → Array s₂
    reshape (mkarr vec) s₂ p = mkarr (subst (Vec A) p vec)

    -- Take from the head of the array.
    take : ∀ {d : ℕ}{s : Shape (1 + d)}
      → (n : ℕ)
      → (p : n ≤ head s)
      → Array s
      → Array (take-shape n s p)
    take {s = x ∷ s} n p (mkarr v) = mkarr (take-vec (n * ∏ s) v helper)
      where
      open Data.Nat.Properties
      helper : n * ∏ s ≤ x * ∏ s
      helper = *-monoˡ-≤ (∏ s) p

    drop : ∀ {d : ℕ}{s : Shape (1 + d)}
      → (n : ℕ)
      → Array s
      → (p : n ≤ head s)
      → Array (drop-shape n s p)
    drop {s = s} zero a _ = a
    drop {s = x ∷ s} (suc n) a p 
      = drop {s = x ∷ s} n a ((≤-trans (n≤1+n n) p))

  module Indexing where
    open Data.Fin hiding (_+_)

    -- This definition doesn't match with the paper.
    ψ : ∀ {k : ℕ}
      → {s : Shape (1 + k)}
      → (idx : Fin (head s))
      → Array s
      → Array (tail s)
    ψ {s = s@(_ ∷ _)} zero  a   
      = reshape (take 1 (s≤s z≤n) a) (tail s) (+-identityʳ (∏ (tail s)))
    ψ {s = s@(_ ∷ _)} (suc pp) a 
      = ψ zero (drop 1 a (s≤s z≤n))

    expand-d-shape
      : ∀ {d} (s : Shape d)
      → (axis : Fin (1 + d))
      → Shape (1 + d)
    expand-d-shape s zero = 1 ∷ s
    expand-d-shape {d = .(suc _)} (s₀ ∷ s) (suc axis) 
      = s₀ ∷  expand-d-shape s axis

    pi-expand-s-pi-s
      : ∀ {d} (s : Shape d)
      → (axis : Fin (1 + d))
      → ∏ (expand-d-shape s axis) ≡ ∏ s
    pi-expand-s-pi-s [] zero = refl
    pi-expand-s-pi-s (x ∷ s) zero = +-identityʳ (x * ∏ s)
    pi-expand-s-pi-s (x ∷ s) (suc axis) 
      = cong (x *_) (pi-expand-s-pi-s s axis)

moa.agda-lib

name: moa
include: .
depend: standard-library

moa.pdf