------------------------------------------------------------------------
-- The Agda standard library
--
-- Container combinators
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Container.Combinator where
open import Data.Container.Core using (Container; Shape; Position; ⟦_⟧)
open import Data.Container.Relation.Unary.Any using (◇; any)
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
open import Data.Product.Base as Product using (_,_; <_,_>; proj₁; proj₂; ∃)
open import Data.Sum.Base as Sum using ([_,_]′)
open import Data.Unit.Polymorphic.Base using (⊤)
import Function.Base as F
open import Level using (Level; _⊔_; lower)
------------------------------------------------------------------------
-- Combinators
module _ {s p : Level} where
-- Identity.
id : Container s p
id .Shape = ⊤
id .Position = F.const ⊤
to-id : ∀ {a} {A : Set a} → F.id A → ⟦ id ⟧ A
to-id x = (_ , λ _ → x)
from-id : ∀ {a} {A : Set a} → ⟦ id ⟧ A → F.id A
from-id xs = proj₂ xs _
-- Constant.
const : Set s → Container s p
const A .Shape = A
const A .Position = F.const ⊥
to-const : ∀ {b} (A : Set s) {B : Set b} → A → ⟦ const A ⟧ B
to-const _ = _, ⊥-elim {Whatever = F.const _}
from-const : ∀ {b} (A : Set s) {B : Set b} → ⟦ const A ⟧ B → A
from-const _ = proj₁
module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
-- Composition.
infixr 9 _∘_
_∘_ : Container (s₁ ⊔ s₂ ⊔ p₁) (p₁ ⊔ p₂)
_∘_ .Shape = ⟦ C₁ ⟧ (Shape C₂)
_∘_ .Position = ◇ C₁ (Position C₂)
to-∘ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) → ⟦ _∘_ ⟧ A
to-∘ (s , f) = ((s , proj₁ F.∘ f) , Product.uncurry (proj₂ F.∘ f) F.∘′ ◇.proof)
from-∘ : ∀ {a} {A : Set a} → ⟦ _∘_ ⟧ A → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A)
from-∘ ((s , f) , g) = (s , < f , Product.curry (g F.∘′ any) >)
-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)
infixr 2 _×_
_×_ : Container (s₁ ⊔ s₂) (p₁ ⊔ p₂)
_×_ .Shape = Shape C₁ Product.× Shape C₂
_×_ .Position = Product.uncurry λ s₁ s₂ → (Position C₁ s₁) Sum.⊎ (Position C₂ s₂)
to-× : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A → ⟦ _×_ ⟧ A
to-× ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ]′)
from-× : ∀ {a} {A : Set a} → ⟦ _×_ ⟧ A → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A
from-× ((s₁ , s₂) , f) = ((s₁ , f F.∘ Sum.inj₁) , (s₂ , f F.∘ Sum.inj₂))
-- Indexed product.
module _ {i s p} (I : Set i) (Cᵢ : I → Container s p) where
Π : Container (i ⊔ s) (i ⊔ p)
Π .Shape = ∀ i → Shape (Cᵢ i)
Π .Position = λ s → ∃ λ i → Position (Cᵢ i) (s i)
to-Π : ∀ {a} {A : Set a} → (∀ i → ⟦ Cᵢ i ⟧ A) → ⟦ Π ⟧ A
to-Π f = (proj₁ F.∘ f , Product.uncurry (proj₂ F.∘ f))
from-Π : ∀ {a} {A : Set a} → ⟦ Π ⟧ A → ∀ i → ⟦ Cᵢ i ⟧ A
from-Π (s , f) = λ i → (s i , λ p → f (i , p))
-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)
infix 0 const[_]⟶_
const[_]⟶_ : ∀ {i s p} → Set i → Container s p → Container (i ⊔ s) (i ⊔ p)
const[ A ]⟶ C = Π A (F.const C)
-- Sum. (Note that, up to isomorphism, this is a special case of
-- indexed sum.)
module _ {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where
infixr 1 _⊎_
_⊎_ : Container (s₁ ⊔ s₂) p
_⊎_ .Shape = (Shape C₁ Sum.⊎ Shape C₂)
_⊎_ .Position = [ Position C₁ , Position C₂ ]′
to-⊎ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A → ⟦ _⊎_ ⟧ A
to-⊎ = [ Product.map Sum.inj₁ F.id , Product.map Sum.inj₂ F.id ]′
from-⊎ : ∀ {a} {A : Set a} → ⟦ _⊎_ ⟧ A → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A
from-⊎ (Sum.inj₁ s₁ , f) = Sum.inj₁ (s₁ , f)
from-⊎ (Sum.inj₂ s₂ , f) = Sum.inj₂ (s₂ , f)
-- Indexed sum.
module _ {i s p} (I : Set i) (C : I → Container s p) where
Σ : Container (i ⊔ s) p
Σ .Shape = ∃ λ i → Shape (C i)
Σ .Position = λ s → Position (C (proj₁ s)) (proj₂ s)
to-Σ : ∀ {a} {A : Set a} → (∃ λ i → ⟦ C i ⟧ A) → ⟦ Σ ⟧ A
to-Σ (i , (s , f)) = ((i , s) , f)
from-Σ : ∀ {a} {A : Set a} → ⟦ Σ ⟧ A → ∃ λ i → ⟦ C i ⟧ A
from-Σ ((i , s) , f) = (i , (s , 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