------------------------------------------------------------------------
-- The Agda standard library
--
-- The Thunk wrappers for sized codata, copredicates and corelations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Thunk where
open import Size using (Size; ∞; Size<_; SizedSet)
open import Relation.Unary.Sized using (_⇒_; ∀[_])
------------------------------------------------------------------------
-- Basic types.
record Thunk {ℓ} (F : SizedSet ℓ) (i : Size) : Set ℓ where
coinductive
field force : {j : Size< i} → F j
open Thunk public
Thunk^P : ∀ {f p} {F : SizedSet f} (P : Size → F ∞ → Set p)
(i : Size) (tf : Thunk F ∞) → Set p
Thunk^P P i tf = Thunk (λ i → P i (tf .force)) i
Thunk^R : ∀ {f g r} {F : SizedSet f} {G : SizedSet g}
(R : Size → F ∞ → G ∞ → Set r)
(i : Size) (tf : Thunk F ∞) (tg : Thunk G ∞) → Set r
Thunk^R R i tf tg = Thunk (λ i → R i (tf .force) (tg .force)) i
------------------------------------------------------------------------
-- Syntax
Thunk-syntax : ∀ {ℓ} → SizedSet ℓ → Size → Set ℓ
Thunk-syntax = Thunk
syntax Thunk-syntax (λ j → e) i = Thunk[ j < i ] e
------------------------------------------------------------------------
-- Basic functions.
-- Thunk is a functor
module _ {p q} {P : SizedSet p} {Q : SizedSet q} where
map : ∀[ P ⇒ Q ] → ∀[ Thunk P ⇒ Thunk Q ]
map f p .force = f (p .force)
-- Thunk is a comonad
module _ {p} {P : SizedSet p} where
extract : ∀[ Thunk P ] → P ∞
extract p = p .force
duplicate : ∀[ Thunk P ⇒ Thunk (Thunk P) ]
duplicate p .force .force = p .force
module _ {p q} {P : SizedSet p} {Q : SizedSet q} where
infixl 1 _<*>_
_<*>_ : ∀[ Thunk (P ⇒ Q) ⇒ Thunk P ⇒ Thunk Q ]
(f <*> p) .force = f .force (p .force)
-- We can take cofixpoints of functions only making Thunk'd recursive calls
module _ {p} (P : SizedSet p) where
cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
cofix f = f λ where .force → cofix f
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