------------------------------------------------------------------------
-- The Agda standard library
--
-- Usage examples of the effectful view of the Sum type
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Sum.Effectful.Examples where
open import Level using (Level; _⊔_; lift; Lift)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
import Data.Sum.Effectful.Left as Sumₗ using (Sumₗ; functor; monad)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad using (RawMonad)
-- Note that these examples are simple unit tests, because the type
-- checker verifies them.
private
module Examplesₗ {a b} {A : Set a} {B : Set b} where
open import Agda.Builtin.Equality
open import Function.Base using (id)
module Sₗ = Sumₗ A b
open RawFunctor Sₗ.functor
-- This type to the right of ⊎ needs to be a "lifted" version of
-- (B : Set b) that lives in the universe (Set (a ⊔ b)).
fmapId : (x : A ⊎ (Lift a B)) → (id <$> x) ≡ x
fmapId (inj₁ x) = refl
fmapId (inj₂ y) = refl
open RawMonad Sₗ.monad
-- Now, let's show that "pure" is a unit for >>=. We use Lift in
-- exactly the same way as above. The data (x : B) then needs to be
-- "lifted" to this new type (Lift B).
pureUnitL : ∀ {x : B} {f : Lift a B → A ⊎ (Lift a B)}
→ (pure (lift x) >>= f) ≡ f (lift x)
pureUnitL = refl
pureUnitR : (x : A ⊎ (Lift a B)) → (x >>= pure) ≡ x
pureUnitR (inj₁ _) = refl
pureUnitR (inj₂ _) = refl
-- And another (limited version of a) monad law...
bindCompose : ∀ {f g : Lift a B → A ⊎ (Lift a B)}
→ (x : A ⊎ (Lift a B))
→ ((x >>= f) >>= g) ≡ (x >>= (λ y → (f y >>= g)))
bindCompose (inj₁ x) = refl
bindCompose (inj₂ y) = refl
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4