The Agda Typeclassopedia: Applicative

Applicative.agda

{-# OPTIONS --without-K --safe #-}

module Applicative where

-- [0] https://wiki.haskell.org/Typeclassopedia#Applicative

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

open import Function using (_∘′_; const; id)

record Applicative (f : Set → Set) : Set₁ where
    infixl 5 _⊛_ _⊛>_ _<⊛_

    field
        pure : ∀ {a : Set} → a → f a
        _⊛_  : ∀ {a b : Set} → f (a → b) → f a → f b

        identity : ∀ {a : Set} (x : f a) → pure id ⊛ x ≡ x
        homomorphism : ∀ {a b : Set} (g : a → b) (x : a)
            → pure g ⊛ pure x ≡ pure (g x)
        interchange : ∀ {a b : Set} (g : f (a → b)) (x : a)
            → g ⊛ pure x ≡ pure (λ g → g x) ⊛ g
        composition : ∀ {a b c : Set} (g : f (b → c)) (h : f (a → b)) (x : f a)
            → g ⊛ (h ⊛ x) ≡ pure (_∘′_) ⊛ g ⊛ h ⊛ x

    liftA2 : ∀ {a b c : Set} → (a → b → c) → f a → f b → f c
    liftA2 g x y = (pure g ⊛ x) ⊛ y

    _⊛>_ : ∀ {a b : Set} → f a → f b → f b
    x ⊛> y = (pure (const id) ⊛ x) ⊛ y

    _<⊛_ : ∀ {a b : Set} → f a → f b → f a
    _<⊛_ = liftA2 const

module Example where
    data Maybe (a : Set) : Set where
        Just    : a → Maybe a
        Nothing : Maybe a

    _⊛_ : ∀ {a b : Set} → Maybe (a → b) → Maybe a → Maybe b
    Just g  ⊛ Just x  = Just (g x)
    Nothing ⊛ x       = Nothing
    g       ⊛ Nothing = Nothing

    applicative : Applicative Maybe
    applicative = record
        { pure = Just
        ; _⊛_  = _⊛_
        ; identity     = λ { (Just x) → refl ; Nothing → refl }
        ; homomorphism = λ { g x → refl }
        ; interchange  = λ { (Just g) x → refl ; Nothing x → refl }
        ; composition  = composition
        }
        where
        composition : ∀ {a b c : Set}
            → ∀ (g : Maybe (b → c)) (h : Maybe (a → b)) (x : Maybe a)
            → (g ⊛ (h ⊛ x)) ≡ (((Just _∘′_ ⊛ g) ⊛ h) ⊛ x)
        composition Nothing  h        x        = refl
        composition (Just g) Nothing  x        = refl
        composition (Just g) (Just h) Nothing  = refl
        composition (Just g) (Just h) (Just x) = refl