From 42bdddf58599fcd16b298ae7bc777d72b651e1ef Mon Sep 17 00:00:00 2001 From: alecsferra Date: Sat, 20 May 2023 15:17:12 +0200 Subject: [PATCH] Initial commit --- .gitignore | 1 + src/Derivative.agda | 16 ++++++++++++++ src/Example/List.agda | 27 +++++++++++++++++++++++ src/Example/Stream.agda | 24 +++++++++++++++++++++ src/FAlgebra.agda | 23 ++++++++++++++++++++ src/FCoAlgebra.agda | 28 ++++++++++++++++++++++++ src/Polynomial.agda | 48 +++++++++++++++++++++++++++++++++++++++++ 7 files changed, 167 insertions(+) create mode 100644 .gitignore create mode 100644 src/Derivative.agda create mode 100644 src/Example/List.agda create mode 100644 src/Example/Stream.agda create mode 100644 src/FAlgebra.agda create mode 100644 src/FCoAlgebra.agda create mode 100644 src/Polynomial.agda diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..171a389 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +*.agdai diff --git a/src/Derivative.agda b/src/Derivative.agda new file mode 100644 index 0000000..a2c52d6 --- /dev/null +++ b/src/Derivative.agda @@ -0,0 +1,16 @@ +module Derivative where + +open import Polynomial using (Polynomial) +open import Data.Unit using (⊤) +open import Data.Empty using (⊥) + +open Polynomial.Polynomial + + +infixl 10 ∂_ + +∂_ : Polynomial → Polynomial +∂ I = K ⊤ +∂ K k = K ⊥ +∂ (L ⊗ R) = ∂ L ⊗ R ⊕ L ⊗ ∂ R +∂ (L ⊕ R) = ∂ L ⊕ ∂ R diff --git a/src/Example/List.agda b/src/Example/List.agda new file mode 100644 index 0000000..2a2616d --- /dev/null +++ b/src/Example/List.agda @@ -0,0 +1,27 @@ +module Example.List where + +open import Polynomial using (Polynomial) +open import FAlgebra using (μ_; cata) +open import Data.Unit using (⊤; tt) +open import Data.Sum using (inj₁; inj₂) +open import Data.Product using (_,_) + +open Polynomial.Polynomial +open μ_ + +List : Set → Set +List A = μ (ListF A) + where + ListF : Set → Polynomial + ListF A = K ⊤ ⊕ K A ⊗ I + +pattern [] = inj₁ tt +pattern _∷_ x xs = inj₂ (x , xs) + +fold : {A B : Set} → (A → B → B) → B → List A → B +fold _*_ z = cata λ{ [] → z + ; (x ∷ xs) → x * xs } + +map : {A B : Set} → (A → B) → List A → List B +map f = cata λ{ [] → μ⟨ [] ⟩ + ; (x ∷ xs) → μ⟨ f x ∷ xs ⟩ } diff --git a/src/Example/Stream.agda b/src/Example/Stream.agda new file mode 100644 index 0000000..25c419b --- /dev/null +++ b/src/Example/Stream.agda @@ -0,0 +1,24 @@ +{-# OPTIONS --guardedness #-} + +module Example.Stream where + +open import Polynomial using (Polynomial) +open import FCoAlgebra using (ν_; ana) +open import Data.Unit using (tt) +open import Data.Product using (_,_; _×_; proj₁; proj₂) + + +open Polynomial.Polynomial +open ν_ + +StreamF : Set → Polynomial +StreamF A = K A ⊗ I + +Stream : Set → Set +Stream A = ν (StreamF A) + +repeat : {A : Set} → A → Stream A +repeat = ana λ{ z → (z , z) } + +map : {A B : Set} → (A → B) → Stream A → Stream B +map {A} {B} f = ana λ{ z → f (proj₁ (rest z)) , proj₂ (rest z) } diff --git a/src/FAlgebra.agda b/src/FAlgebra.agda new file mode 100644 index 0000000..067b70b --- /dev/null +++ b/src/FAlgebra.agda @@ -0,0 +1,23 @@ +module FAlgebra where + +open import Polynomial using (Polynomial; ⟦_⟧) +open import Data.Sum using (inj₁; inj₂) +open import Data.Product using (_,_) + +open Polynomial.Polynomial + +data μ_ (F : Polynomial) : Set where + μ⟨_⟩ : ⟦ F ⟧ (μ F) → μ F + +Algebra : Polynomial → Set → Set +Algebra F A = ⟦ F ⟧ A → A + +cata : {F : Polynomial} {A : Set} → Algebra F A → μ F → A +cata {F} ϕ μ⟨ x ⟩ = ϕ (mapCata F F ϕ x) + where + mapCata : ∀ {X} F G → Algebra G X → ⟦ F ⟧ (μ G) → ⟦ F ⟧ X + mapCata I G ϕ μ⟨ x ⟩ = ϕ (mapCata G G ϕ x) + mapCata (K C) G ϕ x = x + mapCata (L ⊕ R) G ϕ (inj₁ xₗ) = inj₁ (mapCata L G ϕ xₗ) + mapCata (L ⊕ R) G ϕ (inj₂ xᵣ) = inj₂ (mapCata R G ϕ xᵣ) + mapCata (L ⊗ R) G ϕ (xₗ , xᵣ) = mapCata L G ϕ xₗ , mapCata R G ϕ xᵣ diff --git a/src/FCoAlgebra.agda b/src/FCoAlgebra.agda new file mode 100644 index 0000000..b9eec06 --- /dev/null +++ b/src/FCoAlgebra.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --guardedness #-} + +module FCoAlgebra where + +open import Polynomial using (Polynomial; ⟦_⟧) +open import Data.Sum using (inj₁; inj₂) +open import Data.Product using (_,_) + +open Polynomial.Polynomial + +record ν_ (F : Polynomial) : Set where + coinductive + field + rest : ⟦ F ⟧ (ν F) +open ν_ + +Co-Algebra : Polynomial → Set → Set +Co-Algebra F A = A → ⟦ F ⟧ A + +ana : {F : Polynomial} {A : Set} → Co-Algebra F A → A → ν F +rest (ana {F} ϕ x) = mapAna F F ϕ (ϕ x) + where + mapAna : ∀ {X} F G → Co-Algebra F X → ⟦ G ⟧ X → ⟦ G ⟧ (ν F) + mapAna F I ϕ x = ana ϕ x + mapAna F (K C) ϕ x = x + mapAna F (L ⊕ R) ϕ (inj₁ xₗ) = inj₁ (mapAna F L ϕ xₗ) + mapAna F (L ⊕ R) ϕ (inj₂ xᵣ) = inj₂ (mapAna F R ϕ xᵣ) + mapAna F (L ⊗ R) ϕ (xₗ , xᵣ) = mapAna F L ϕ xₗ , mapAna F R ϕ xᵣ diff --git a/src/Polynomial.agda b/src/Polynomial.agda new file mode 100644 index 0000000..df8c058 --- /dev/null +++ b/src/Polynomial.agda @@ -0,0 +1,48 @@ +module Polynomial where + +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Data.Product using (_×_; _,_) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl) +open import Function using (_∘_; id) + + +infixl 6 _⊕_ +infixl 7 _⊗_ +infixl 8 _⊙_ + + +data Polynomial : Set₁ where + I : Polynomial + K : Set → Polynomial + _⊗_ : Polynomial → Polynomial → Polynomial + _⊕_ : Polynomial → Polynomial → Polynomial + +_⊙_ : Polynomial → Polynomial → Polynomial +I ⊙ G = G +K k ⊙ G = K k +(L ⊗ R) ⊙ G = L ⊙ G ⊗ R ⊙ G +(L ⊕ R) ⊙ G = L ⊙ G ⊕ R ⊙ G + +⟦_⟧ : Polynomial → Set → Set +⟦ I ⟧ x = x +⟦ K k ⟧ x = k +⟦ L ⊗ R ⟧ x = ⟦ L ⟧ x × ⟦ R ⟧ x +⟦ L ⊕ R ⟧ x = ⟦ L ⟧ x ⊎ ⟦ R ⟧ x + +⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ : (F G : Polynomial) → ⟦ F ⊙ G ⟧ ≡ ⟦ F ⟧ ∘ ⟦ G ⟧ +⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ I G = refl +⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (K k) G = refl +⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (L ⊗ R) G rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ L G + rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ R G + = refl +⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ (L ⊕ R) G rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ L G + rewrite ⟦F⊙G⟧≡⟦F⟧∙⟦G⟧ R G + = refl + +map : (F : Polynomial) → {X Y : Set} → (X → Y) → ⟦ F ⟧ X → ⟦ F ⟧ Y +map I f x = f x +map (K k) f x = x +map (L ⊗ R) f (xₗ , xᵣ) = map L f xₗ , map R f xᵣ +map (L ⊕ R) f (inj₁ xₗ) = inj₁ (map L f xₗ) +map (L ⊕ R) f (inj₂ xᵣ) = inj₂ (map R f xᵣ)