Add more instances

This commit is contained in:
Frederik Hanghøj Iversen 2017-06-07 21:49:54 +02:00
parent 8485b55152
commit 38fd690839
2 changed files with 84 additions and 15 deletions

@ -1 +1 @@
Subproject commit 62cf020f9ea7b3e3d78612222402a782f222bb04
Subproject commit e46610eda0bbdebb072a70b947742f765a335b01

View file

@ -3,8 +3,9 @@ module Cat where
open import Agda.Primitive
open import Prelude.Function
import Prelude.Equality
-- import Prelude.Equality
open import PathPrelude
open ≡-Reasoning
-- Questions:
--
@ -12,18 +13,21 @@ open import PathPrelude
-- in Agda (like undefined in Haskell).
--
-- Does Agda have a way to specify local submodules?
--
-- Can I open parts of a record, like say:
--
-- open Functor {{...}} ( fmap )
record Functor {a b} (F : Set a Set b) : Set (lsuc a b) where
field
-- morphisms
fmap : {A B} (A B) F A F B
-- laws
identity : { A : Set a } -> id fmap (id { A = A })
-- Why does PathPrelude.≡ not agree with Prelude.Equality.≡
fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B ) -> fmap f fmap g fmap (f g)
-- fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B ) -> fmap f ∘ fmap g Prelude.Equality.≡ fmap (f ∘ g)
identity : { A : Set a }
-> id fmap (id { A = A })
fusion : { A B C : Set a } ( f : B -> C ) ( g : A -> B )
-> fmap f fmap g fmap (f g)
-- PathPrelude._≡_ : {a : Level} {A : Set a} → A → A → Set a
-- Prelude.Equality._≡_ : {a : Level} {A : Set a} → A → A → Set a
open Functor {{ ... }} hiding ( identity )
_<$>_ : {a b : Level} {F : Set a Set b} {{r : Functor F}} {A B : Set a} (A B) F A F B
@ -58,9 +62,34 @@ instance
Functor.fmap MaybeFunctor f nothing = nothing
Functor.fmap MaybeFunctor f (just x) = just (f x)
-- how the heck can I use `fun-ext` which produces `Path id (fmap id)` wheras the type of the whole is `id ≡ fmap id`.
Functor.identity MaybeFunctor = (fun-ext (λ { nothing refl ; (just x) refl }))
-- Why can I not use `fun-ext` here?
Functor.fusion MaybeFunctor f g = {!!} -- fun-ext (λ { nothing -> refl ; (just x) -> refl })
Functor.identity MaybeFunctor = fun-ext (λ { nothing refl ; (just x) refl })
Functor.fusion MaybeFunctor f g = fun-ext (λ
-- Why does inlining `lem₀` give rise to an error?
{ nothing lem₀
; (just x) {! refl!}
{- ; (just x) → begin
(fmap f fmap g) (just x) ≡⟨⟩
(fmap f (fmap g (just x))) ≡⟨⟩
(fmap f (just (g x))) ≡⟨⟩
(just (f (g x))) ≡⟨⟩
just ((f g) x) ∎-}
})
where
lem₀ : nothing nothing
lem₀ = refl
-- `lem₁` and `fusionjust` are the same.
lem₁ : {A B C : Set} {f : B C} {g : A B} {x : A}
just (f (g x)) just (f (g x))
lem₁ = refl
fusionjust : { A B C : Set } { x : A } { f : B -> C } { g : A -> B }
-> (fmap f fmap g) (just x) just ((f g) x)
fusionjust {x = x} {f = f} {g = g} = begin
(fmap f fmap g) (just x) ≡⟨⟩
(fmap f (fmap g (just x))) ≡⟨⟩
(fmap f (just (g x))) ≡⟨⟩
(just (f (g x))) ≡⟨⟩
just ((f g) x)
record Applicative {a} (F : Set a -> Set a) : Set (lsuc a) where
field
@ -70,18 +99,58 @@ record Applicative {a} (F : Set a -> Set a) : Set (lsuc a) where
-- laws
-- `ap-identity` is paraphrased from the documentation for Applicative on hackage.
ap-identity : { A : Set a } -> ap (pure (id { A = A })) id
composition : { A B C : Set a } { u : F (B -> C) } { v : F (A -> B) } { w : F A }
composition : { A B C : Set a } ( u : F (B -> C) ) ( v : F (A -> B) ) ( w : F A )
-> ap (ap (ap (pure _∘_) u) v) w ap u (ap v w)
homomorphism : { A B : Set a } { a : A } { f : A -> B }
-> ap (pure f) (pure a) pure (f a)
interchange : { A B : Set a } { u : F (A -> B) } { a : A }
interchange : { A B : Set a } ( u : F (A -> B) ) ( a : A )
-> ap u (pure a) ap (pure (_$ a)) u
open Applicative {{...}}
_<*>_ = ap
instance
IdentityApplicative : Applicative Identity
Applicative.pure IdentityApplicative = identity
Applicative.ap IdentityApplicative (identity f) (identity a) = identity (f a)
Applicative.ap-identity IdentityApplicative = refl
Applicative.composition IdentityApplicative = refl
Applicative.composition IdentityApplicative _ _ _ = refl
Applicative.homomorphism IdentityApplicative = refl
Applicative.interchange IdentityApplicative = refl
Applicative.interchange IdentityApplicative _ _ = refl
-- Is this provable? How?
-- I suppose this would be `≡`'s functor-instance.
equiv-app : {A B : Set} -> {f g : A -> B} -> {a : A} -> f g -> f a g a
equiv-app f≡g = {!!}
instance
MaybeApplicative : Applicative Maybe
Applicative.pure MaybeApplicative = just
Applicative.ap MaybeApplicative nothing _ = nothing
Applicative.ap MaybeApplicative (just f) x = fmap f x
-- Why does termination-check fail when I use `refl` in both cases below?
Applicative.ap-identity MaybeApplicative = fun-ext (λ
{ nothing {!refl!}
; (just x) {!refl!}
})
Applicative.composition MaybeApplicative nothing v w = refl
Applicative.composition MaybeApplicative (just x) nothing w = refl
-- Easy-mode:
-- Applicative.composition MaybeApplicative {u = just f} {just g} {nothing} = refl
-- Applicative.composition MaybeApplicative {u = just f} {just g} {just x} = refl
-- Re-use mode:
Applicative.composition MaybeApplicative (just f) (just g) w = sym (equiv-app lem)
where
lem : {A B C} {f : B C} {g : A B} {w : Maybe A}
(fmap f) (fmap g)
(Functor.fmap MaybeFunctor (f g))
lem = Functor.fusion MaybeFunctor _ _
{-
Applicative.composition MaybeApplicative { u = u } { v = v } { w = w } = begin
ap (ap (ap (pure _∘_) u) v) w ≡⟨⟩
ap (ap (fmap _∘_ u) v) w ≡⟨ {!!}
{!!}
-}
Applicative.homomorphism MaybeApplicative = refl
Applicative.interchange MaybeApplicative nothing a = refl
Applicative.interchange MaybeApplicative (just x) a = refl