------------------------------------------------------------------------
-- The Agda standard library
--
-- The Stream type and some operations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Stream where
open import Codata.Sized.Thunk as Thunk using (Thunk; force)
open import Data.Nat.Base using (ℕ; suc; zero)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _∷⁺_)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.Product.Base as P using (Σ; _×_; _,_; <_,_>; proj₁; proj₂)
open import Function.Base using (id; _∘_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Size using (Size; ∞; Size<_)
private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
i : Size
------------------------------------------------------------------------
-- Type
data Stream (A : Set a) (i : Size) : Set a where
_∷_ : A → Thunk (Stream A) i → Stream A i
infixr 5 _∷_
------------------------------------------------------------------------
-- Creating streams
repeat : A → Stream A i
repeat a = a ∷ λ where .force → repeat a
infixr 5 _++_ _⁺++_
_++_ : List A → Stream A i → Stream A i
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ where .force → xs ++ ys
unfold : (A → A × B) → A → Stream B i
unfold next seed =
let (seed′ , b) = next seed in
b ∷ λ where .force → unfold next seed′
iterate : (A → A) → A → Stream A ∞
iterate f = unfold < f , id >
nats : Stream ℕ ∞
nats = iterate suc zero
------------------------------------------------------------------------
-- Looking at streams
head : Stream A i → A
head (x ∷ xs) = x
tail : {j : Size< i} → Stream A i → Stream A j
tail (x ∷ xs) = xs .force
lookup : Stream A ∞ → ℕ → A
lookup xs zero = head xs
lookup xs (suc k) = lookup (tail xs) k
------------------------------------------------------------------------
-- Transforming streams
map : (A → B) → Stream A i → Stream B i
map f (x ∷ xs) = f x ∷ λ where .force → map f (xs .force)
ap : Stream (A → B) i → Stream A i → Stream B i
ap (f ∷ fs) (x ∷ xs) = f x ∷ λ where .force → ap (fs .force) (xs .force)
scanl : (B → A → B) → B → Stream A i → Stream B i
scanl c n (x ∷ xs) = n ∷ λ where .force → scanl c (c n x) (xs .force)
zipWith : (A → B → C) → Stream A i → Stream B i → Stream C i
zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ λ where .force → zipWith f (as .force) (bs .force)
------------------------------------------------------------------------
-- List⁺-related functions
_⁺++_ : List⁺ A → Thunk (Stream A) i → Stream A i
(x ∷ xs) ⁺++ ys = x ∷ λ where .force → xs ++ ys .force
cycle : List⁺ A → Stream A i
cycle xs = xs ⁺++ λ where .force → cycle xs
concat : Stream (List⁺ A) i → Stream A i
concat (xs ∷ xss) = xs ⁺++ λ where .force → concat (xss .force)
------------------------------------------------------------------------
-- Chunking
splitAt : (n : ℕ) → Stream A ∞ → Vec A n × Stream A ∞
splitAt zero xs = [] , xs
splitAt (suc n) (x ∷ xs) = P.map₁ (x ∷_) (splitAt n (xs .force))
take : (n : ℕ) → Stream A ∞ → Vec A n
take n xs = proj₁ (splitAt n xs)
drop : ℕ → Stream A ∞ → Stream A ∞
drop n xs = proj₂ (splitAt n xs)
chunksOf : (n : ℕ) → Stream A ∞ → Stream (Vec A n) ∞
chunksOf n = chunksOfAcc n id module ChunksOf where
chunksOfAcc : ∀ k (acc : Vec A k → Vec A n) →
Stream A ∞ → Stream (Vec A n) i
chunksOfAcc zero acc xs = acc [] ∷ λ where .force → chunksOfAcc n id xs
chunksOfAcc (suc k) acc (x ∷ xs) = chunksOfAcc k (acc ∘ (x ∷_)) (xs .force)
------------------------------------------------------------------------
-- Interleaving streams
-- The most basic of interleaving strategies is to take two streams and
-- alternate between emitting values from one and the other.
interleave : Stream A i → Thunk (Stream A) i → Stream A i
interleave (x ∷ xs) ys = x ∷ λ where .force → interleave (ys .force) xs
-- This interleaving strategy can be generalised to an arbitrary
-- non-empty list of streams
interleave⁺ : List⁺ (Stream A i) → Stream A i
interleave⁺ xss =
List⁺.map head xss
⁺++ λ where .force → interleave⁺ (List⁺.map tail xss)
-- To generalise this further to a stream of streams however we have to
-- adopt a different strategy: if we were to start with *all* the heads
-- then we would never reach any of the second elements in the streams.
-- Here we use Cantor's zig zag function to explore the plane defined by
-- the function `(i,j) ↦ lookup (lookup xss i) j‵ mapping coordinates to
-- values in a way that guarantees that any point is reached in a finite
-- amount of time. The definition is taken from the paper:
-- Applications of Applicative Proof Search by Liam O'Connor
cantor : Stream (Stream A ∞) ∞ → Stream A ∞
cantor (l ∷ ls) = zig (l ∷ []) (ls .force) module Cantor where
zig : List⁺ (Stream A ∞) → Stream (Stream A ∞) ∞ → Stream A i
zag : List⁺ A → List⁺ (Stream A ∞) → Stream (Stream A ∞) ∞ → Stream A i
zig xss = zag (List⁺.map head xss) (List⁺.map tail xss)
zag (x ∷ []) zs (l ∷ ls) = x ∷ λ where .force → zig (l ∷⁺ zs) (ls .force)
zag (x ∷ (y ∷ xs)) zs ls = x ∷ λ where .force → zag (y ∷ xs) zs ls
-- We can use the Cantor zig zag function to define a form of `bind'
-- that reaches any point of the plane in a finite amount of time.
plane : {B : A → Set b} → Stream A ∞ → ((a : A) → Stream (B a) ∞) →
Stream (Σ A B) ∞
plane as bs = cantor (map (λ a → map (a ,_) (bs a)) as)
-- Here is the beginning of the path we are following:
_ : take 21 (plane nats (λ _ → nats))
≡ (0 , 0)
∷ (1 , 0) ∷ (0 , 1)
∷ (2 , 0) ∷ (1 , 1) ∷ (0 , 2)
∷ (3 , 0) ∷ (2 , 1) ∷ (1 , 2) ∷ (0 , 3)
∷ (4 , 0) ∷ (3 , 1) ∷ (2 , 2) ∷ (1 , 3) ∷ (0 , 4)
∷ (5 , 0) ∷ (4 , 1) ∷ (3 , 2) ∷ (2 , 3) ∷ (1 , 4) ∷ (0 , 5)
∷ []
_ = refl
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4