The Agda Typeclassopedia: Functor

Functor.agda

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

module Functor where

-- [0] https://wiki.haskell.org/Typeclassopedia#Functor
-- [1] https://wiki.haskell.org/Typeclassopedia#Laws
-- [2] https://github.com/quchen/articles/blob/master/second_functor_law.md

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

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

-- I will try to keep naming similar to what Brent Yorgey proposed in the
-- Typeclassopedia: `f` is used only for functors `g` and `h` (and others as
-- needed) for functions.
record Functor (f : Set → Set) : Set₁ where
    infixl 5 _<$>_ _<$_
    infixl 1 _<&>_

    field
        fmap : ∀ {a b : Set} → (a → b) → f a → f b
        -- Guarantees that `fmap` preserves the functor's structure [1].
        identity : ∀ {a : Set} (x : f a) → fmap id x ≡ x

    {-
    -- Commented because I don't know how to proof the free theorem.
    postulate
        free-theorem : ∀ {a b b′ c : Set}
            → ∀ (g : b → c) (h : a → b) (p : b′ → c) (q : a → b′)
            → (∀ x → g (h x) ≡ p (q x))
            → (∀ x → fmap g (fmap h x) ≡ fmap p (fmap q x))

    -- The second functor law: follows from the first one [2].
    composition : ∀ {a b c : Set} (g : b → c) (h : a → b) (x : f a)
        → fmap (g ∘ h) x ≡ fmap g (fmap h x)
    composition g h x
        rewrite free-theorem g h id (g ∘ h) (λ x′ → refl) x
              | identity (fmap (g ∘ h) x) = refl
    -}

    -- Definitions of little interest.
    _<$>_ = fmap

    _<$_ : ∀ {a b : Set} → a → f b → f a
    x <$ y = const x <$> y

    _<&>_ : ∀ {a b : Set} → f a → (a → b) → f b
    _<&>_ = flip _<$>_

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

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

    functor : Functor Maybe
    functor = record
        { fmap = fmap
        ; identity = λ { (Just x) → refl ; Nothing → refl }
        }