{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import Equational

module Applicative (F : Set → Set)

       (fmap   : {A B : Set} → (A → B) → F A → F B)
       (pure   : {A : Set} → A → F A)
       (_<*>_  : {A B : Set} → F (A → B) → F A → F B) 

-- applicative functor law

       (fmapLaw         : {A B : Set} → {g : A → B} → {fa : F A} → fmap g fa ≡ pure g <*> fa)
       (identityLaw     : {A : Set} → {fa : F A} → Extensionality → pure id <*> fa ≡ fa)
       (compositionLaw  : {A B C : Set} → {fa : F A} → {fbc : F (B → C)} → {fab : F (A → B)} → Extensionality
                          → ((pure (_∘_) <*> fbc) <*> fab) <*> fa ≡ fbc <*> (fab <*> fa))
       (homomorphismLaw : {A B : Set} → {f : A → B} → {a : A} → pure f <*> pure a ≡ pure (f a))
       (interchangeLaw  : {A B : Set} → {fab : F (A → B)} → {a : A} → Extensionality
                          → fab <*> pure a ≡ pure (applyTo a) <*> fab)

where

functorLaw1 : {A : Set} → {fa : F A} → Extensionality → fmap id fa ≡ fa
functorLaw1 {_} {fa} ext  = fmap id fa
                                           ≡⟨ fmapLaw ⟩
                            pure id <*> fa
                                           ≡⟨ identityLaw ext ⟩
                            fa
                                           QED


functorLaw2 : {A B C : Set} → {f : A → B} → {g : B → C} → {fa : F A} → Extensionality
              → fmap (g ∘ f) fa ≡ fmap g (fmap f fa)

functorLaw2 {_} {_} {_} {f} {g} {fa} ext =

   fmap (g ∘ f) fa
                                                ≡⟨ fmapLaw ⟩
   pure (g ∘ f) <*> fa
                                                ≡⟨ cong (flip _<*>_ fa) (sym homomorphismLaw) ⟩
   (pure (_∘_ g) <*> pure f) <*> fa
                                                ≡⟨ cong (flip _<*>_ fa ∘ flip _<*>_ (pure f)) (sym homomorphismLaw) ⟩
   ((pure _∘_ <*> pure g) <*> pure f) <*> fa
                                                ≡⟨ compositionLaw ext ⟩
   pure g <*> (pure f <*> fa)
                                                ≡⟨ cong (_<*>_ (pure g)) (sym fmapLaw) ⟩
   pure g <*> fmap f fa
                                                ≡⟨ sym fmapLaw ⟩
   fmap g (fmap f fa)
                                                QED

import Pointed
open Pointed F fmap pure functorLaw1 functorLaw2 public

fmap2 : {A B C : Set} → (A → B → C) → F A → F B → F C
fmap2 f a b = fmap f a <*> b

fmap3 : {A B C D : Set} → (A → B → C → D) → F A → F B → F C → F D
fmap3 f a b c = fmap2 f a b <*> c

fmap4 : {A B C D E : Set} → (A → B → C → D → E) → F A → F B → F C → F D → F E
fmap4 f a b c d = fmap3 f a b c <*> d