open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base

open import Meta.Traversable
open import Meta.Invariant
open import Meta.Idiom
open import Meta.Bind
open import Meta.Alt

module Data.Maybe.Base where

The Maybe type🔗

private variable
  ℓ ℓ' : Level
  A B C : Type ℓ

data Maybe {ℓ} (A : Type ℓ) : Type ℓ where
  nothing : Maybe A
  just    : A → Maybe A

{-# BUILTIN MAYBE Maybe #-}

instance
  Map-Maybe : Map (eff Maybe)
  Map-Maybe .map f (just x) = just (f x)
  Map-Maybe .map f nothing  = nothing

  Idiom-Maybe : Idiom (eff Maybe)
  Idiom-Maybe .Idiom.Map-idiom = Map-Maybe

  Idiom-Maybe .Idiom.pure  = just

  Idiom-Maybe .Idiom._<*>_ (just f) (just x) = just (f x)
  Idiom-Maybe .Idiom._<*>_ (just f) nothing  = nothing
  Idiom-Maybe .Idiom._<*>_ nothing  _        = nothing

  Bind-Maybe : Bind (eff Maybe)
  Bind-Maybe .Bind.Idiom-bind = Idiom-Maybe

  Bind-Maybe ._>>=_ (just x) f = f x
  Bind-Maybe ._>>=_ nothing  f = nothing

  Alt-Maybe : Alt (eff Maybe)
  Alt-Maybe .Alt.fail = nothing
  Alt-Maybe .Alt._<|>_ (just x) y = just x
  Alt-Maybe .Alt._<|>_ nothing y = y

  Traversable-Maybe : Traversable (eff Maybe)
  Traversable-Maybe .Traversable.traverse f nothing  = pure nothing
  Traversable-Maybe .Traversable.traverse f (just x) = just <$> f x

Maybe-rec : (A → B) → B → Maybe A → B
Maybe-rec f b (just x) = f x
Maybe-rec f b nothing = b

from-just : A → Maybe A → A
from-just def (just x) = x
from-just def nothing = def

is-just : Maybe A → Type
is-just (just _) = ⊤
is-just nothing = ⊥

is-nothing : Maybe A → Type
is-nothing (just _) = ⊥
is-nothing nothing = ⊤

nothing≠just : {x : A} → ¬ (nothing ≡ just x)
nothing≠just p = subst is-nothing p tt

just≠nothing : {x : A} → ¬ (just x ≡ nothing)
just≠nothing p = subst is-just p tt

just-inj : ∀ {x y : A} → just x ≡ just y → x ≡ y
just-inj {x = x} = ap (from-just x)

instance
  Discrete-Maybe : ⦃ d : Discrete A ⦄ → Discrete (Maybe A)
  Discrete-Maybe {x = just x} {just y}   = invmap (ap just) just-inj (x ≡? y)
  Discrete-Maybe {x = just x} {nothing}  = no just≠nothing
  Discrete-Maybe {x = nothing} {just x}  = no nothing≠just
  Discrete-Maybe {x = nothing} {nothing} = yes refl

Pointed types as Maybe-algebras🔗

maybe→alt : ∀ {M : Effect} {ℓ} {A : Type ℓ}
          → ⦃ _ : Alt M ⦄ ⦃ _ : Idiom M ⦄ → Maybe A → M .Effect.₀ A
maybe→alt (just x) = pure x
maybe→alt nothing  = fail

maybe-injective : Maybe A ≃ Maybe B → A → B
maybe-injective e x with inspect (e .fst (just x))
... | just y , _ = y
... | nothing , p with inspect (e .fst nothing)
... | just y  , _ = y
... | nothing , q = absurd (just≠nothing (Equiv.injective₂ e p q))