0 | ||| Version of Maybe indexed by an `isJust' boolean
 1 | module Data.IMaybe
 2 |
 3 | import Data.Zippable
 4 |
 5 | %default total
 6 |
 7 | public export
 8 | data IMaybe : Bool -> Type -> Type where
 9 |   Just : a -> IMaybe True a
10 |   Nothing : IMaybe False a
11 |
12 | public export
13 | fromJust : IMaybe True a -> a
14 | fromJust (Just a) = a
15 |
16 | public export
17 | Functor (IMaybe b) where
18 |   map f (Just a) = Just (f a)
19 |   map f Nothing = Nothing
20 |
21 | public export
22 | Applicative (IMaybe True) where
23 |   pure = Just
24 |   Just f <*> Just x = Just (f x)
25 |
26 | public export
27 | Zippable (IMaybe b) where
28 |   zipWith f Nothing  Nothing  = Nothing
29 |   zipWith f (Just x) (Just y) = Just $ f x y
30 |
31 |   zipWith3 f Nothing  Nothing  Nothing  = Nothing
32 |   zipWith3 f (Just x) (Just y) (Just z) = Just $ f x y z
33 |
34 |   unzipWith f Nothing  = (Nothing, Nothing)
35 |   unzipWith f (Just x) = let (a, b) = f x in (Just a, Just b)
36 |
37 |   unzipWith3 f Nothing  = (Nothing, Nothing, Nothing)
38 |   unzipWith3 f (Just x) = let (a, b, c) = f x in (Just a, Just b, Just c)
39 |