------------------------------------------------------------------------
-- The Maybe type
------------------------------------------------------------------------

module Data.Maybe where

------------------------------------------------------------------------
-- The type

data Maybe (A : Set) : Set where
just    : (x : A)  Maybe A
nothing : Maybe A

------------------------------------------------------------------------
-- Some operations

open import Data.Bool
open import Data.Unit

boolToMaybe : Bool  Maybe
boolToMaybe true  = just _
boolToMaybe false = nothing

maybeToBool :  {A}  Maybe A  Bool
maybeToBool (just _) = true
maybeToBool nothing  = false

-- A non-dependent eliminator.

maybe : {a b : Set}  (a  b)  b  Maybe a  b
maybe j n (just x) = j x
maybe j n nothing  = n

maybe₀₁ : {a : Set} {b : Set1}  (a  b)  b  Maybe a  b
maybe₀₁ j n (just x) = j x
maybe₀₁ j n nothing  = n

------------------------------------------------------------------------

open import Data.Function
open import Category.Functor

MaybeFunctor : RawFunctor Maybe
MaybeFunctor = record
{ _<\$>_ = λ f  maybe (just  f) nothing
}

{ return = just
; _>>=_  = _>>=_
}
where
_>>=_ :  {a b}  Maybe a  (a  Maybe b)  Maybe b
nothing >>= f = nothing
just x  >>= f = f x

;      = nothing
}

; _∣_       = _∣_
}
where
_∣_ :  {a}  Maybe a  Maybe a  Maybe a
nothing  y = y
just x   y = just x

------------------------------------------------------------------------
-- Equality

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

drop-just :  {A} {x y : A}  just x  just y  x  y
drop-just ≡-refl = ≡-refl

decSetoid :  {A}  Decidable (_≡_ {A})  DecSetoid
decSetoid {A} _A-≟_ = ≡-decSetoid _≟_
where
_≟_ : Decidable (_≡_ {Maybe A})
just x   just y  with x A-≟ y
just x   just .x | yes ≡-refl = yes ≡-refl
just x   just y  | no  x≢y    = no (x≢y  drop-just)
just x   nothing = no λ()
nothing  just y  = no λ()
nothing  nothing = yes ≡-refl