List as Funtor

List.Agda

{-# OPTIONS --type-in-type #-}
{-# OPTIONS --no-import-sorts #-}
module Foo where
open import Agda.Primitive renaming (Set to Type)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong₂)
open import Data.Product using (_×_; _,_) renaming (proj₁ to π₁; proj₂ to π₂)

postulate  Extensionality : {A : Type} {B : A → Type} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

REL : Type -> Type -> Type 
REL A B = A -> B -> Type 

Rel :  Type -> Type 
Rel A  = REL A A 

-- Precategory (need to parameterize with equality)
record Category : Type where
  field
    Ob : Type 
    _⇒_ : Rel Ob
    _∘_  : ∀ {x y z : Ob} -> y ⇒ z -> x ⇒ y -> x ⇒ z
    id : ∀ {o : Ob} -> o ⇒ o
    idˡ : ∀ {x y : Ob} (f : x ⇒ y) -> f ∘ (id {x}) ≡ f
    idʳ : ∀ {x y : Ob} (f : x ⇒ y) -> (id {y}) ∘ f ≡ f
    ∘-assoc : ∀ {x y z w : Ob} (f : x ⇒ y) (g : y ⇒ z) (h : z ⇒ w) -> h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
open Category

record Functor (𝒞 𝒟 : Category) : Type where
    private 
        module C = Category 𝒞
        module D = Category 𝒟
    field
        F₀ : C.Ob -> D.Ob
        F₁ : ∀ {A B} (f : C._⇒_ A B ) -> D._⇒_ (F₀ A) (F₀ B)

        identity : ∀ {A} -> (F₁ (C.id {A})) ≡ D.id {(F₀ A)}
        homomorphism : ∀ {A B C} -> (f : C._⇒_ A B) -> (g : C._⇒_ B C) ->
            F₁ (C._∘_ g f) ≡ D._∘_ (F₁ g) (F₁ f)


-- Here is a Category where the objects are Types and the morphisms are functions 
Agda : Category
Agda = record
        { Ob = Type
        ; _⇒_ = λ x y → (x → y)
        ; _∘_ = λ g f x → g (f x)
        ; id = λ x → x
        ; idˡ = λ f → refl
        ; idʳ = λ f → refl
        ; ∘-assoc = λ f g h → refl 
        }


data List (A : Type) : Type where 
    nil : List A
    cons : A → List A → List A

list-fmap : {A B : Type} → (A → B) → List A → List B
list-fmap f nil = nil
list-fmap f (cons x xs) = cons (f x ) (list-fmap f xs)

prf₁ : {A : Agda .Ob} → (xs : List A) → list-fmap (Agda .id) xs ≡ (Agda .id) xs
prf₁ nil = refl
prf₁ (cons x xs) = cong (cons x) (prf₁  xs)

prf₂ : {A B C : Agda .Ob} (f : Agda ._⇒_ A B) (g : Agda ._⇒_ B C)(xs : List A) → list-fmap ((Agda ._∘_) g f) xs ≡ ((Agda ._∘_) (list-fmap g) (list-fmap f)) xs
prf₂ f g nil = refl
prf₂ f g (cons x xs) = cong (cons (g (f x))) (prf₂ f g xs)

List-is-Functor : Functor Agda Agda
List-is-Functor = record {
                    F₀ = List; -- List : Type → Type
                    F₁ = list-fmap ; -- (f : A → B) → List A → List B
                    identity =  Extensionality prf₁ ; 
                    homomorphism = λ f g → Extensionality λ x → prf₂ f g x} 


-- ^ above is the usual categorical model of a functional programming language 
-- DTC leverages the fact that we can make data constructors of a type into Functors 
module DTC where 
    {-  compared to this
        data List (A : Type) : Type where 
            nil : List A
            cons : A → List A → List A

        previously we saide List : Type → Type was a functor.

        Now we will make the constructors `nil` and `cons` into Functors
        then we can reconstruct the `List` type by taking Least Fixed Point of the Coproduct of the Nil and Cons functors
    
    -}
    data Nil (A : Type) : Type where 
        nil : Nil A

    data Cons (A B : Type) : Type where 
        cons : A → B → Cons A B

    {-# NO_POSITIVITY_CHECK #-}
    data Fix (F : Type → Type) : Type where
        In : F (Fix F) → Fix F
    open Fix

    -- Coproduct of functors F G (coproduct in a Functor Category)
    data _⊹_ (F G : Type → Type) (E : Type) : Type where 
        Inl : F E → _⊹_ F G E 
        Inr : G E → _⊹_ F G E
    open _⊹_

    -- ListF as a coproduct of Nil and Cons functors
    ListF : Type → Type → Type
    ListF A = Nil ⊹ Cons A

    List' : Type → Type
    List' A = Fix (ListF A)

    -- "smart constructors"
    nil' : {A : Type} → List' A 
    nil' = In (Inl nil)

    cons' : {A : Type} → A → List' A → List' A 
    cons' x xs = In (Inr (cons x xs))

    open import Data.Nat
    -- Example of the recovered list type
    ex : List' ℕ
    ex = cons' 3 (cons' 4 nil') 



    Nil-is-Functor : Functor Agda Agda
    Nil-is-Functor = record { 
        F₀ = Nil ; 
        F₁ =  λ f x → nil; 
        identity = Extensionality λ { nil → refl} ; 
        homomorphism = λ f g → Extensionality λ { nil  → refl }
        }

    Cons-is-Functor : (X : Ob Agda) → Functor Agda Agda
    Cons-is-Functor X = record { 
        F₀ = Cons X ; 
        F₁ = λ{ f (cons x xs) → cons x (f xs)} ; 
        identity = Extensionality λ{ (cons x x₁) → refl }; 
        homomorphism = λ f g → Extensionality λ{ (cons x x₁) → refl} }


    -- coproduct of functors is a functor
    ⊹-Functor : (F G : Functor Agda Agda)→ Functor Agda Agda
    ⊹-Functor 
        record { F₀ = F-F₀ ; F₁ = F-F₁ ; identity = F-id ; homomorphism = F-hom }  
        record { F₀ = G-F₀ ; F₁ = G-F₁ ; identity = G-id; homomorphism = G-hom }  
        = record { 
            F₀ = F-F₀ ⊹ G-F₀ ;  
            F₁ = λ{f (Inl x) → Inl (F-F₁ f x)
                 ; f (Inr x) → Inr (G-F₁ f x) };   
            identity = Extensionality λ{ (Inl x) → {!    !}
                                       ; (Inr x) → {!   !}} ; 
            homomorphism = {!   !} 
        } 

    ListF-is-Functor : (X : Ob Agda) → Functor Agda Agda
    ListF-is-Functor X = ⊹-Functor Nil-is-Functor (Cons-is-Functor X)