maybe.agda

module maybe where

open import level
open import eq
open import bool

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data maybe {ℓ}(A : Set ℓ) : Set ℓ where
  nothing : maybe A
  just : A → maybe A

{-# FOREIGN GHC type AgdaMaybe l = Maybe #-}
-- ^ Deal with maybe's level-polymorphism (the ℓ implicit parameter)
{-# COMPILE GHC maybe = data AgdaMaybe (Nothing | Just) #-}

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

_≫=maybe_ : ∀ {ℓ}{A B : Set ℓ} → maybe A → (A → maybe B) → maybe B
nothing ≫=maybe f = nothing
(just x) ≫=maybe f = f x

return-maybe : ∀ {ℓ}{A : Set ℓ} → A → maybe A
return-maybe a = just a

down-≡ : ∀{ℓ}{A : Set ℓ}{a a' : A} → just a ≡ just a' → a ≡ a'
down-≡ refl = refl

isJust : ∀{ℓ}{A : Set ℓ} → maybe A → 𝔹
isJust nothing = ff
isJust (just _) = tt

maybe-extract : ∀{ℓ}{A : Set ℓ} → (x : maybe A) → isJust x ≡ tt → A
maybe-extract (just x) p = x
maybe-extract nothing ()

maybe-map : ∀{ℓ}{A B : Set ℓ} → (A → B) → maybe A → maybe B
maybe-map f (just x) = just (f x)
maybe-map f nothing = nothing