Test

test.agda

module _ where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)

open import Data.Nat
  using (ℕ; zero; suc)

open import Data.Empty
  using (⊥; ⊥-elim)

open import Data.Sum
  using (_⊎_; inj₁; inj₂)

open import Data.Product
  using (_×_; _,_; proj₁; proj₂)

open import plfa.part1.Isomorphism
  using (_≃_; _∘_; extensionality)

module MyFunctors where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Function using (_°_; id)

record Functor (F : Set → Set) : Set₁ where
    field
        fmap : ∀ {A B : Set} → (A → B) → F A → F B
        fmapid : ∀ {A : Set} (f : F A) → fmap id f ≡ f
        fmap° : ∀ {A B C : Set} (f : (A → B)) (g : (B → C)) (x : F A) → fmap (g ° f) x ≡ (fmap g ° fmap f) x

open Functor

record Applicative (F : Set → Set) : Set₁ where
    field
        functor : Functor F
        pure : ∀ {A : Set} → A → F A
        _<*>_ : ∀ {A B : Set} → F (A → B) → F A → F B
        ap-id : ∀ {A : Set} {v : F A} → pure id <*> v ≡ v
        ap-homo : ∀ {A B : Set} {f : (A → B)} {x : A} → pure f <*> pure x ≡ pure (f x)
        ap-xchange : ∀ {A B : Set} {x : A} {ff : F (A → B)} → ff <*> pure x ≡ Functor.fmap functor (λ f → f x) ff

open Applicative

record Monad (F : Set → Set) : Set₁ where
    field
        applicative : Applicative F
        join : ∀ {A : Set} → F (F A) → F A
        join°pure : ∀ {A : Set} {x : F A} → join (Applicative.pure applicative x) ≡ x

open Monad


data Maybe (A : Set) : Set where
    Nothing : Maybe A
    Just : A → Maybe A

data IdF (A : Set) : Set where
    idf : A → IdF A

data Const (A : Set) (B : Set) : Set where
    constf : A → Const A B

data List (A : Set) : Set where
    []  : List A
    _∷_ : (x : A) → (xs : List A) → List A


id-functor : Functor IdF
id-functor = record
    { fmap = λ { f (idf x) → idf (f x) }
    ; fmapid = λ { (idf x) → refl }
    ; fmap° = λ { f g (idf x) → refl }
    }

maybe-functor : Functor Maybe
maybe-functor = record
    { fmap = λ { f Nothing → Nothing
               ; f (Just x) → Just (f x) }
    ; fmapid = λ { Nothing → refl
                 ; (Just x) → refl }
    ; fmap° = λ {f g Nothing → refl
               ; f g (Just x) → refl}
    }

const-functor : ∀ {C : Set} → Functor (Const C)
const-functor = record
    { fmap = λ { f (constf x) → constf x }
    ; fmapid = λ { (constf x) → refl }
    ; fmap° = λ { f g (constf x) → refl }
    }

list-fmap : ∀ {A B : Set} → (A → B) → List A → List B
list-fmap _ [] = []
list-fmap f (x ∷ xs) = f x ∷ list-fmap f xs

list-fmap-id : ∀ {A : Set} (x : List A) → list-fmap id x ≡ x
list-fmap-id [] = refl
list-fmap-id (x ∷ xs) = cong (x ∷_) (list-fmap-id xs)

list-fmap-° : ∀ {A B C : Set} (f : A → B) (g : B → C) (xs : List A) →
    list-fmap (g ° f) xs ≡ list-fmap g (list-fmap f xs)

list-fmap-° f g [] = refl
list-fmap-° f g (x ∷ xs) = cong ((g ° f) x ∷_) (list-fmap-° f g xs)

list-functor : Functor List
list-functor = record
    { fmap = list-fmap
    ; fmapid = list-fmap-id
    ; fmap° = list-fmap-°
    }


list-functor' : Functor List
list-functor' = record
    { fmap = λ { f [] → []
               ; f (x ∷ xs) → {! (f x) ∷ (fmap f xs) !} } -- ???
    ; fmapid = {!   !}
    ; fmap° = {!   !}
    }

{-
Error:
(A → B) !=< (Functor _F_180)
when checking that the expression f has type Functor _F_180
-}