------------------------------------------------------------------------ -- Another implementation of the Fibonacci sequence using tail, along -- with some other examples ------------------------------------------------------------------------ module ArbitraryChunks where open import Coinduction open import Data.Bool open import Data.Nat open import Data.Stream as S using (Stream; _≈_; _∷_) open import Data.Vec as V using (Vec; []; _∷_) open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; inspect; _with-≡_) ------------------------------------------------------------------------ -- Stream programs -- StreamP m n A encodes programs generating streams in chunks of size -- (at least) m, where the first chunk has size (at least) n. infixr 5 _∷_ data StreamP (m : ℕ) : ℕ → Set → Set₁ where [_] : ∀ {A} (xs : ∞ (StreamP m m A)) → StreamP m 0 A _∷_ : ∀ {n A} (x : A) (xs : StreamP m n A) → StreamP m (suc n) A forget : ∀ {n A} (xs : StreamP m (suc n) A) → StreamP m n A tail : ∀ {n A} (xs : StreamP m (suc n) A) → StreamP m n A zipWith : ∀ {n A B C} (f : A → B → C) (xs : StreamP m n A) (ys : StreamP m n B) → StreamP m n C map : ∀ {n A B} (f : A → B) (xs : StreamP m n A) → StreamP m n B data StreamW (m : ℕ) : ℕ → Set → Set₁ where [_] : ∀ {A} (xs : StreamP m m A) → StreamW m 0 A _∷_ : ∀ {n A} (x : A) (xs : StreamW m n A) → StreamW m (suc n) A forgetW : ∀ {m n A} → StreamW (suc m) (suc n) A → StreamW (suc m) n A forgetW {n = zero} (x ∷ [ xs ]) = [ x ∷ forget xs ] forgetW {n = suc n} (x ∷ xs) = x ∷ forgetW xs tailW : ∀ {m n A} → StreamW m (suc n) A → StreamW m n A tailW (x ∷ xs) = xs zipWithW : ∀ {m n A B C} → (A → B → C) → StreamW m n A → StreamW m n B → StreamW m n C zipWithW f [ xs ] [ ys ] = [ zipWith f xs ys ] zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWithW f xs ys mapW : ∀ {m n A B} → (A → B) → StreamW m n A → StreamW m n B mapW f [ xs ] = [ map f xs ] mapW f (x ∷ xs) = f x ∷ mapW f xs whnf : ∀ {m n A} → StreamP (suc m) n A → StreamW (suc m) n A whnf [ xs ] = [ ♭ xs ] whnf (x ∷ xs) = x ∷ whnf xs whnf (forget xs) = forgetW (whnf xs) whnf (tail xs) = tailW (whnf xs) whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys) whnf (map f xs) = mapW f (whnf xs) mutual ⟦_⟧W : ∀ {m n A} → StreamW (suc m) (suc n) A → Stream A ⟦ x ∷ [ xs ] ⟧W = x ∷ ♯ ⟦ xs ⟧P ⟦ x ∷ (y ∷ xs) ⟧W = x ∷ ♯ ⟦ y ∷ xs ⟧W ⟦_⟧P : ∀ {m n A} → StreamP (suc m) (suc n) A → Stream A ⟦ xs ⟧P = ⟦ whnf xs ⟧W ------------------------------------------------------------------------ -- Some examples -- The Fibonacci sequence. fib : StreamP 1 1 ℕ fib = 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget fib) (tail fib)) ] -- Some sequence which is defined using (tail ∘ tail). someSequence : StreamP 2 2 ℕ someSequence = 0 ∷ 1 ∷ [ ♯ (1 ∷ 2 ∷ zipWith _+_ (tail (tail someSequence)) (forget (forget someSequence))) ] ------------------------------------------------------------------------ -- The definition of fib is correct -- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith. mutual zipWithW-hom : ∀ {m n A B C} (_∙_ : A → B → C) (xs : StreamW (suc m) (suc n) A) ys → ⟦ zipWithW _∙_ xs ys ⟧W ≈ S.zipWith _∙_ ⟦ xs ⟧W ⟦ ys ⟧W zipWithW-hom _∙_ (x ∷ [ xs ]) (y ∷ [ ys ]) = (x ∙ y) ∷ ♯ zipWith-hom _∙_ xs ys zipWithW-hom _∙_ (x ∷ x′ ∷ xs) (y ∷ y′ ∷ ys) = (x ∙ y) ∷ ♯ zipWithW-hom _∙_ (x′ ∷ xs) (y′ ∷ ys) zipWith-hom : ∀ {m n A B C} (_∙_ : A → B → C) (xs : StreamP (suc m) (suc n) A) ys → ⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P zipWith-hom _∙_ xs ys = zipWithW-hom _∙_ (whnf xs) (whnf ys) -- forget is the identity on streams. open import MapIterate using (_≈P_; _∷_; _≈⟨_⟩_; _∎; soundP) open import Relation.Binary.PropositionalEquality as P using (_≡_; _with-≡_) mutual forgetW-lemma : ∀ {m n A} x (xs : StreamW (suc m) (suc n) A) → ⟦ x ∷ forgetW xs ⟧W ≈P x ∷ ♯ ⟦ xs ⟧W forgetW-lemma x (x′ ∷ [ xs ]) = x ∷ ♯ (_ ≈⟨ forget-lemma x′ xs ⟩ x′ ∷ ♯ (_ ∎)) forgetW-lemma x (x′ ∷ x″ ∷ xs) = x ∷ ♯ (_ ≈⟨ forgetW-lemma x′ (x″ ∷ xs) ⟩ x′ ∷ ♯ (_ ∎) ) forget-lemma : ∀ {m n A} x (xs : StreamP (suc m) (suc n) A) → ⟦ x ∷ forget xs ⟧P ≈P x ∷ ♯ ⟦ xs ⟧P forget-lemma x xs with P.inspect (whnf xs) ... | (y ∷ y′ ∷ ys) with-≡ eq rewrite eq = x ∷ ♯ helper where helper : ⟦ y ∷ forgetW (y′ ∷ ys) ⟧W ≈P ⟦ xs ⟧P helper rewrite eq = _ ≈⟨ forgetW-lemma y (y′ ∷ ys) ⟩ y ∷ ♯ (_ ∎) ... | (y ∷ [ ys ]) with-≡ eq rewrite eq = x ∷ ♯ helper where helper : ⟦ y ∷ forget ys ⟧P ≈P ⟦ xs ⟧P helper rewrite eq = _ ≈⟨ forget-lemma y ys ⟩ y ∷ ♯ (_ ∎) -- The stream ⟦ fib ⟧P satisfies its intended defining equation. open import Relation.Binary module SS {A : Set} = Setoid (S.setoid A) fib-correct : ⟦ fib ⟧P ≈ 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (S.tail ⟦ fib ⟧P)) fib-correct = 0 ∷ ♯ (1 ∷ ♯ SS.trans (zipWith-hom _+_ (0 ∷ forget fib′) fib′) (S.zipWith-cong _+_ (SS.trans (soundP (forget-lemma 0 fib′)) (0 ∷ ♯ SS.refl)) SS.refl)) where fib′ = 1 ∷ zipWith _+_ (forget fib) (tail fib) ------------------------------------------------------------------------ -- map₂ -- A variant of S.map which processes streams in chunks of size 2. map₂ : ∀ {A B} → (A → B) → Stream A → Stream B map₂ f (x ∷ xs) with ♭ xs map₂ f (x ∷ xs) | y ∷ ys = f x ∷ ♯ (f y ∷ ♯ map₂ f (♭ ys)) -- This function is extensionally equal to S.map. map≈map₂ : ∀ {A B} → (f : A → B) → (xs : Stream A) → S.map f xs ≈ map₂ f xs map≈map₂ f (x ∷ xs) with inspect (♭ xs) map≈map₂ f (x ∷ xs) | (y ∷ ys) with-≡ eq rewrite eq = f x ∷ ♯ helper eq where map-f-y∷ys = _ helper : ∀ {xs} → xs ≡ y ∷ ys → S.map f xs ≈ map-f-y∷ys helper refl = f y ∷ ♯ map≈map₂ f (♭ ys) -- However, as explained in "Beating the Productivity Checker Using -- Embedded Languages", the two functions are not interchangeable -- (assuming that pattern matching is evaluated strictly). Let us see -- what happens when we use the language above. We can define the -- stream of natural numbers using chunks of size 1 and 2. nats : StreamP 1 1 ℕ nats = 0 ∷ [ ♯ map suc nats ] nats₂ : StreamP 2 2 ℕ nats₂ = 0 ∷ 1 ∷ [ ♯ map suc nats₂ ] -- The first use of map corresponds to S.map, and the second to map₂. -- If we try to use map₂ in the first definition, then we get a type -- error. The following code is not accepted. -- nats : StreamP 2 1 ℕ -- nats = 0 ∷ [ ♯ map suc nats ]