gistfile1.agda

module experiment where

open import Agda.Primitive
open import Prelude.List
open import Prelude.Size
open import Prelude.Monoidal
open import Prelude.Monad
open import Prelude.Functor
open import Prelude.Natural
open Size using (∞)
open Π using (_∘_)


mutual
  data Delay ..(i : Size) (A : Set) : Set where
    now : A → Delay i A
    later : ∞Delay i A → Delay i A

  record ∞Delay ..(i : Size) (A : Set) : Set where
    coinductive
    field
      force : ..{j : Size.< i} → Delay j A

open Delay public
open ∞Delay public

mutual
  never : ∀ {A} → Delay ∞ A
  never = later ∞never

  ∞never : ∀ {A} → ∞Delay ∞ A
  force ∞never = never


mutual
  Delay-bind : ∀ {i A B} → Delay i A →  (A → Delay i B) → Delay i B
  Delay-bind (now a) f = f a
  Delay-bind (later a∞) f = later (∞Delay-bind a∞ f)

  ∞Delay-bind : ∀ {i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
  force (∞Delay-bind a∞ f) = Delay-bind (force a∞) f

instance
  Delay-functor : Functor (Delay ∞)
  Functor.map Delay-functor f x = Delay-bind x (now ∘ f)

instance
  Delay-monad : Monad (Delay ∞)
  (Monad.return Delay-monad) a = now a
  Monad.bind Delay-monad k m = Delay-bind m k

mutual
  _⋏_ : ∀ {A} → Delay ∞ A → Delay ∞ A → Delay ∞ A
  now x ⋏ y = now x
  later x ⋏ now y = now y
  later x ⋏ later y = later (x ∞⋏ y)

  _∞⋏_ : ∀ {A} → ∞Delay ∞ A → ∞Delay ∞ A → ∞Delay ∞ A
  force (x ∞⋏ y) = (force x ⋏ force y)


-- Capretta / "General Recursion via Coinductive Types"
mutual
  parallel-search-aux : ∀ {A} → (Nat → Delay ∞ A) → Nat → Delay ∞ A → Delay ∞ A
  parallel-search-aux f n (now x) = now x
  parallel-search-aux f n (later x) = later (∞parallel-search-aux f (su n) (force x ⋏ f n))

  ∞parallel-search-aux : ∀ {A} → (Nat → Delay ∞ A) → Nat → Delay ∞ A → ∞Delay ∞ A
  force (∞parallel-search-aux f n x) = parallel-search-aux f n x


⨆ : ∀ {A} → (Nat → Delay ∞ A) → Delay ∞ A
⨆ f = parallel-search-aux f 0 never