Coinductive records

{-# OPTIONS --cubical-compatible --guardedness #-}
open import Data.Sum
open import Data.Maybe as Maybe
open import Data.Nat
open import Relation.Binary.PropositionalEquality

open import Function.Base

Another option to model partiality, using coinduction. This was moved to a separate file to remove the --guardedness from

open import Partial

module _ where
private
  variable
    A B C : Set

Streams

record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A

fromℕ→A : (ℕ → A) → Stream A
Stream.hd (fromℕ→A f) = f 0
Stream.tl (fromℕ→A f) = fromℕ→A (f ∘ suc)

toℕ→A : Stream A → (ℕ → A)
toℕ→A s zero = Stream.hd s
toℕ→A s (suc k) = toℕ→A (Stream.tl s) k

Delay

record Delay (A : Set) : Set where
  coinductive
  field
    try : Delay A ⊎ A

module Delay⇒Stepped where
  f : Delay A → ℕ → Maybe A
  f d zero = nothing
  f d (suc k) =
    case Delay.try d of λ
    { (inj₁ d') → f d' k
    ; (inj₂ a) → just a
    }
  f-mono : ∀ d → is-mono (f {A} d)
  f-mono d (suc k) fdk-just with (Delay.try d)
  ... | inj₁ d' = f-mono d' k fdk-just
  ... | inj₂ y = refl

  step-indexed : Delay A → Step-Indexed A
  step-indexed d = record { f = f d ; f-mono = f-mono d }

module Stepped⇒Delay where
  delayed : Step-Indexed A → Delay A
  Delay.try (delayed s) =
    case f 0 of λ
    { (just x) → inj₂ x
    ; nothing → inj₁ (delayed (record
      { f = f ∘ suc
      ; f-mono = f-mono ∘ suc
      }))
    }
    where
      open Step-Indexed s

[End of lecture on 9 July 2026] Agda Quellcode herunterladen