1 files changed, 45 insertions, 7 deletions
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index 33317e5..b399444 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -17,12 +17,17 @@ data Maybe {a} (A : Set a) : Set a where
 {-# FOREIGN GHC type AgdaMaybe a b = Maybe b #-}
 {-# COMPILE GHC Maybe = data MAlonzo.Code.Data.Maybe.Base.AgdaMaybe (Just | Nothing) #-}
 
+open import Function
+open import Agda.Builtin.Equality using (_≡_ ; refl)
+
+just-injective : ∀ {a} {A : Set a} {a b} → (Maybe A ∋ just a) ≡ just b → a ≡ b
+just-injective refl = refl
+
 ------------------------------------------------------------------------
 -- Some operations
 
 open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Unit.Base using (⊤)
-open import Function
 open import Relation.Nullary
 
 boolToMaybe : Bool → Maybe ⊤
@@ -52,16 +57,23 @@ maybe j n nothing  = n
 maybe′ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B
 maybe′ = maybe
 
+-- A defaulting mechanism
+
+fromMaybe : ∀ {a} {A : Set a} → A → Maybe A → A
+fromMaybe = maybe′ id
+
 -- A safe variant of "fromJust". If the value is nothing, then the
 -- return type is the unit type.
 
-From-just : ∀ {a} (A : Set a) → Maybe A → Set a
-From-just A (just _) = A
-From-just A nothing  = Lift ⊤
+module _ {a} {A : Set a} where
 
-from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just A x
-from-just (just x) = x
-from-just nothing  = _
+  From-just : Maybe A → Set a
+  From-just (just _) = A
+  From-just nothing  = Lift a ⊤
+
+  from-just : (x : Maybe A) → From-just x
+  from-just (just x) = x
+  from-just nothing  = _
 
 -- Functoriality: map.
 
@@ -93,3 +105,29 @@ to-witness (just {x = p} _) = p
 to-witness-T : ∀ {p} {P : Set p} (m : Maybe P) → T (is-just m) → P
 to-witness-T (just p) _  = p
 to-witness-T nothing  ()
+
+------------------------------------------------------------------------
+-- Aligning and Zipping
+
+open import Data.These using (These; this; that; these)
+open import Data.Product hiding (zip)
+
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
+
+  alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C
+  alignWith f (just a) (just b) = just (f (these a b))
+  alignWith f (just a) nothing  = just (f (this a))
+  alignWith f nothing  (just b) = just (f (that b))
+  alignWith f nothing  nothing  = nothing
+
+  zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
+  zipWith f (just a) (just b) = just (f a b)
+  zipWith _ _ _ = nothing
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+  align : Maybe A → Maybe B → Maybe (These A B)
+  align = alignWith id
+
+  zip : Maybe A → Maybe B → Maybe (A × B)
+  zip = zipWith _,_