module GenericProgramming where open import Data.Product renaming (map to pmap) open import Data.Sum renaming (map to smap) data Functor : Set₁ where |Id| : Functor |K| : (A : Set) → Functor _|+|_ : (F : Functor) → (G : Functor) → Functor _|×|_ : (F : Functor) → (G : Functor) → Functor ⟦_⟧ : Functor → Set → Set ⟦ |Id| ⟧ X = X ⟦ (|K| A) ⟧ X = A ⟦ (F |+| G) ⟧ X = ⟦ F ⟧ X ⊎ ⟦ G ⟧ X ⟦ (F |×| G) ⟧ X = ⟦ F ⟧ X × ⟦ G ⟧ X map : ∀ (F : Functor) {X Y : Set} → (X → Y) → ⟦ F ⟧ X → ⟦ F ⟧ Y map |Id| φ x = φ x map (|K| A) φ x = x map (F |+| G) φ (inj₁ x) = inj₁ (map F φ x) map (F |+| G) φ (inj₂ y) = inj₂ (map G φ y) map (F |×| G) φ (x , y) = map F φ x , map G φ y data μ_ (F : Functor) : Set where <_> : ⟦ F ⟧ (μ F) → μ F record True : Set where NatF = |K| True |+| |Id| NAT = μ NatF Z : NAT Z = < inj₁ _ > S : NAT → NAT S n = < inj₂ n > {-# NON_TERMINATING #-} fold' : ∀ (F : Functor) {X : Set} → (⟦ F ⟧ X → X) → μ F → X fold' F φ < x > = φ (map F (fold' F φ) x) ListF = λ A → |K| True |+| (|K| A |×| |Id|) LIST = λ A → μ (ListF A) nil : {A : Set} → LIST A nil = < inj₁ _ > cons : {A : Set} → A → LIST A → LIST A cons x xs = < inj₂ (x , xs) >