module Data.Type.Option where
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Maybe
data Option (f :: k -> *) :: Maybe k -> * where
Nothing_ :: Option f Nothing
Just_ :: !(f a) -> Option f (Just a)
deriving instance MaybeC (Eq <$> f <$> m) => Eq (Option f m)
deriving instance
( MaybeC (Eq <$> f <$> m)
, MaybeC (Ord <$> f <$> m)
) => Ord (Option f m)
deriving instance MaybeC (Show <$> f <$> m) => Show (Option f m)
option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r
option j n = \case
Just_ a -> j a
Nothing_ -> n
instance Functor1 Option where
map1 f = \case
Just_ a -> Just_ $ f a
Nothing_ -> Nothing_
instance Foldable1 Option where
foldMap1 f = \case
Just_ a -> f a
Nothing_ -> mempty
instance Traversable1 Option where
traverse1 f = \case
Just_ a -> Just_ <$> f a
Nothing_ -> pure Nothing_
instance Known (Option f) Nothing where
known = Nothing_
instance Known f a => Known (Option f) (Just a) where
type KnownC (Option f) (Just a) = Known f a
known = Just_ known
instance (Witness p q (f a), x ~ Just a) => Witness p q (Option f x) where
type WitnessC p q (Option f x) = Witness p q (f (FromJust x))
(\\) r = \case
Just_ a -> r \\ a