What does this compute?

Haskell's mapAccumL

mapAccumL :: (s -> a -> (s,b)) -> s -> [a] -> (s, [b])
mapAccumL _ s []     = (s, [])
mapAccumL f s (x:xs) = (s″,y:ys)
                       where (s′, y ) = f s x
                             (s″,ys) = mapAccumL f s′ xs
						

mapAccL in Agda (λ₁)

mapAccL : ∀ n (f : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) (s : λ₁ σ) (xs : λ₁ (vec ρ n))
			→ λ₁ (σ ⊗ vec τ n)
mapAccL zero     _ s _  = s ， []
mapAccL (suc n′) f s xs = case[] xs of λ x xs′ →
                            case⊗ (f s x) of λ s′ y →
                              case⊗ (mapAccL n′ f s′ xs′) of λ s″ ys′ →
                                s″ ， (y ∷ ys′)
						

Definitions and notation

• Universe of types for circuit I/O
• Unit, base type, sums, products
• Notation for object type vars: σₙ, τₙ, ρₙ

data Uₚ (B : Set) : Set where
  𝟙     : Uₚ B
  ι     : Uₚ B
  _⊗_   : (τ₁ τ₂ : Uₚ B) → Uₚ B
  _⊕_   : (τ₁ τ₂ : Uₚ B) → Uₚ B

Tₚ : ∀ {B} (τ : Uₚ B) → Set
Tₚ      𝟙          = ⊤
Tₚ {B}  ι          = B
Tₚ      (τ₁ ⊗ τ₂)  = Tₚ τ₁  × Tₚ τ₂
Tₚ      (τ₁ ⊕ τ₂)  = Tₚ τ₁  ⊎ Tₚ τ₂
						

Context, Environments and Gates

• A Ctxt is a list of Uₚ
• An Env is a heterogenous list indexed by a Ctxt
• Contexts: Γₙ, Δₙ,…
• Environments: γₙ, δₙ,…
• A Gate has an interface (Δ,τ) and a spec (⟦–⟧g)

record Gate {B} (Δ : Ctxt B) (τ : Uₚ B) : Set where
  constructor MkG
  field  ⟦–⟧g : Env Tₚ Δ → Tₚ τ

ONE : ∀ {B} → Gate {B} ε 𝟙
ONE = MkG constOne
  where  constOne : ∀ {B} (γ : Env {B} Tₚ ε) → Tₚ {⊤} 𝟙
         constOne = const tt
						

The "Lambda1" EDSL

• Core datatype (λ₁′) indexed by inputs, output
• De Bruijn indices, let's for sharing, explicit looping construct
• Products, sums, fundamental gates
• No arrow types: no lambda, no application

data λ₁′ {B} : (Γ : Ctxt B) (τ : Uₚ B) → Set where
  [_]    : ∀ {Γ τ}                (i : Γ ∋ τ)
                                   → λ₁′ Γ τ

  letₓ′  : ∀ {Γ σ τ}    (x : λ₁′ Γ σ)  (b : λ₁′ (σ ◅ Γ) τ)
                                   → λ₁′ Γ τ

  loop′  : ∀ {Γ σ τ}       (c : λ₁′ (σ ◅ Γ) (σ ⊗ τ))
                                  → λ₁′ Γ τ
						

Lambda1 surface language

• De Bruijn isn't so friendly
• So we transform Agda binders into binders of the EDSL
• Using the "unembedding" technique by Lindley et al., plus syntax

λ₁ : ∀ {B} (τ : Uₚ B) → Set
λ₁ {B} τ = ∀ {Γ : Ctxt B} → λ₁′ Γ τ

letₓ : ∀ {B} {σ τ} (x : λ₁ σ) (f : λ₁ σ → λ₁ τ) → λ₁ {B} τ
syntax letₓ eₓ (λ x → b) = let͘ x ≔ eₓ in͘ b

loop : ∀ {B} {σ τ} (f : λ₁ σ → λ₁ (σ ⊗ τ)) → λ₁ {B} τ
syntax loop {σ = σ} (λ s → b) = loop s ∶ σ in͘ b

fork : ∀ {B} {τ} (x : λ₁ τ) → λ₁ {B} (τ ⊗ τ)
fork x = let͘ y ≔ x in͘ (y ， y)
						

Back to examples for a while

• Remember mapAccL

Sequential mapAccL

• We can easily define a sequential version of mapAccL
• In mapAccL-seq, there's a loop instead of recursion

• But what does the delay mean?

Semantics, one step at a time

• Loops mean circuits can have state
• Semantics in the state monad
• There's an inductive family giving the state type of a circuit

⟦_⟧s : (c : λ₁′ Γ τ) (s : λₛ c) (γ : Env Tₚ Γ) → (λₛ c × Tₚ τ)
						

data λₛ {B} : {Γ : Ctxt B} {τ : Uₚ B} (c : λ₁′ Γ τ) → Set where
  [_]ₛ   : ∀ {Γ σ}     (i : Γ ∋ σ)                            → λₛ [ i ]
  letₛ   : ∀ {Γ σ τ}   {x : λ₁′ Γ σ} {e : λ₁′ (σ ◅ Γ) τ}  (xₛ : λₛ x) (eₛ : λₛ e)
                                                            → λₛ (letₓ′ x e)

  loopₛ  : ∀ {Γ σ τ}   {c : λ₁′ (σ ◅ Γ) (σ ⊗ τ)}         (iₛ : Tₚ σ) (cₛ : λₛ c)
                                                            → λₛ (loop′ c)

  _，ₛ_   : ∀ {Γ τ₁ τ₂}  {x : λ₁′ Γ τ₁} {y : λ₁′ Γ τ₂}        (xₛ : λₛ x) (yₛ : λₛ y)
                                                              → λₛ (x ，′ y)
						

Circuits in (discrete) time: n steps

• One state transition per clock cycle
• We can simulate a number of cycles with ⟦_⟧n
• Final state is exposed
• Usefulness clear soon

⟦_⟧n : (c : λ₁′ Γ τ) (s : λₛ c) (γn : Vec (Env Tₚ Γ) n) → λₛ c × Vec (Tₚ τ) n
⟦_⟧n n c s = mapAccumL n s ⟦ c ⟧s
						

Parallel vs. sequential

• Now it's almost obvious how mapAccL and mapAccL are related
• In one step from mapAccL, in n steps from mapAccL-seq
• But the exact relation is not so short…

mapAccL-seq : (f : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)) (x : λ₁ ρ) → λ₁ τ
mapAccL-seq {σ} f x = loop s ∶ σ in f s x
						

Par. vs. seq.: mapAccL vs. mapAccL-seq

_⊒_ : ∀ {α β φ : Set} → φ × (α × β) → α × β → Set
(_ , sa,ra) ⊒ sb,rb = sa,ra ≡ sb,rb
						

n : ℕ
X : λₛ (mapAccL n f)

σ ρ τ : Uₚ
f     : λ₁ σ → λ₁ ρ → λ₁ (σ ⊗ τ)
s     : Tₚ σ
xs    : Tₚ (vec ρ n)

MALSt  : Tₚ σ → λₛ (mapAccL-seq {σ} f)
MALIns : Tₚ (vec ρ n) → Vec (Env Tₚ (ρ ◅ ε)) n

⟦ mapAccL n f ⟧s X (↦ s ◅ ↦ xs ◅ ε) ⊒ ⟦ mapAccL-seq f ⟧n n (MALSt s) (MALIns xs)
						

From mapAccL, lots of others…

iterate : ∀ n (f : λ₁ τ → λ₁ τ) (x : λ₁ τ) → λ₁ (vec τ (suc n))
iterate n {τ} f x = mapAccL n f′ x (replicate unit)
  where  f′ : λ₁ τ → λ₁ 𝟙 → λ₁ (τ ⊗ τ)
         f′ x _ = fork (f x)
							

Sequential version: iterate-seq

iterate-seq : (f : λ₁ τ → λ₁ τ) → λ₁ τ
iterate-seq {τ} f = mapAccL-seq f′ unit
  where  f′ : λ₁ τ → λ₁ 𝟙 → λ₁ (τ ⊗ τ)
         f′ x _ = fork (f x)
							

If intermediate results don't matter: repeat

	repeat : ∀ n (f : λ₁ τ → λ₁ τ) → λ₁ τ
	repeat n f x  = fst (iterate n f x)
							

repeat-seq is a little interesting

• We say that intermediate results don't matter
• So the output stream elements from y₀ to yₙ₋₁ don't matter
• We only require that yₙ = fⁿ(x)
• In particular, they can be the intermediate results…

repeat : (f : λ₁ τ → λ₁ τ) → λ₁ τ
repeat-seq = iterate-seq
						

proj₂ (⟦ repeat n f ⟧s X (↦ x ◅ ε)) ≡ proj₁ (⟦ repeat-seq f ⟧n n (repSt x)  emptys)
						

Folds and scans, all-in-one

Definitions: foldl×scanl, foldl, scanl

foldl×scanl : ∀ n (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (e : λ₁ τ) (xs : λ₁ (vec τ n))
              → λ₁ (τ ⊗ vec τ (suc n))
foldl×scanl zero     _⊞_ e _  = e ， (e ∷ [])
foldl×scanl (suc n′) _⊞_ e xs = case⊗ mapAccL (suc n′) f′ e xs of λ fold sums′ →
                                  fold ， (e ∷ sums′)
  where f′ : λ₁ τ → λ₁ τ → λ₁ (τ ⊗ τ)
        f′ acc x = fork (acc ⊞ x)
							

foldl : ∀ n (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (e : λ₁ τ) (xs : λ₁ (vec τ n)) → λ₁ τ
foldl n _⊞_ e = fst (foldl×scanl n _⊞_ e)
							

scanl : ∀ n (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (e : λ₁ τ) (xs : λ₁ (vec τ n))
        → λ₁ (vec τ (suc n))
scanl n _⊞_ e xs = snd (foldl×scanl n _⊞_ e)
							

Sequential version: foldl×scanl

• Interesting extra "shift": extra value in front of the stream

scanl-seq : (_⊞_ : λ₁ τ → λ₁ τ → λ₁ τ) (x : λ₁ τ) → λ₁ τ
scanl-seq _⊞_ x = comp (mapAccL-seq f′ x) shift
  where  f′ : λ₁ τ → λ₁ τ → λ₁ (τ ⊗ τ)
         f′ acc x = fork (acc ⊞ x)
							

Composition and pipelining

• Pardon the flipped composition, it makes things easier…

comp : (f : λ₁ σ → λ₁ ρ) (g : λ₁ ρ → λ₁ τ) → (λ₁ σ → λ₁ τ)
comp = flip _∘_
							

compD : (f : λ₁ σ → λ₁ ρ) (g : λ₁ ρ → λ₁ τ) → (λ₁ σ → λ₁ τ)
compD f g = comp (comp f shift) g
							

Correctness of pipelining

• Here the whole output Stream really matters
• The pipelined version should be shifted by one time unit

⟦ comp f g ⟧* (stComp sf sg) γ ≈ tail (⟦ compD f g ⟧* (stCompD sf sg sd) γ)
							

N-ary composition

• Type-aligned sequence: VecA F as bs
• fs : VecA F as bs = [f₀ : F a₀ b₀, f₁ : F a₁ b₁, …

compN : let F = λ σ τ → (λ₁ σ → λ₁ τ)
        in (fs : VecA F σs τs) → λ₁ (head σs) → λ₁ (last τs))
compN (f ∷ fs′) = comp …
						

⟦ compN fs ⟧* (stCompN n sf) γ ≈ drop n (⟦ compDN fs ⟧* (stCompDN n sf sd) γ)