Initial commit

.gitignore

@@ -0,0 +1 @@
+*.agdai

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

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 ⟩ }

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) }

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ᵣ

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ᵣ

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ᵣ)