module Type.Family.Maybe where
import Type.Family.Constraint
import Type.Family.Monoid
import Type.Class.Witness
type family MaybeC (mc :: Maybe Constraint) :: Constraint where
MaybeC Nothing = ØC
MaybeC (Just c) = c
type family IsNothing (a :: Maybe k) :: Bool where
IsNothing Nothing = True
IsNothing (Just a) = False
nothingCong :: (a ~ b) :- (IsNothing a ~ IsNothing b)
nothingCong = Sub Wit
nothingNotJust :: (Nothing ~ Just a) :- Fail
nothingNotJust = nothingCong
type family (f :: k -> l) <$> (a :: Maybe k) :: Maybe l where
f <$> Nothing = Nothing
f <$> Just a = Just (f a)
infixr 4 <$>
maybeFmapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))
maybeFmapCong = Sub Wit
type family (f :: Maybe (k -> l)) <&> (a :: k) :: Maybe l where
Nothing <&> a = Nothing
Just f <&> a = Just (f a)
infixl 5 <&>
maybePamfCong :: (f ~ g,a ~ b) :- ((f <&> a) ~ (g <&> b))
maybePamfCong = Sub Wit
type family (f :: Maybe (k -> l)) <*> (a :: Maybe k) :: Maybe l where
Nothing <*> a = Nothing
f <*> Nothing = Nothing
Just f <*> Just a = Just (f a)
infixr 4 <*>
maybeApCong :: (f ~ g,a ~ b) :- ((f <*> a) ~ (g <*> b))
maybeApCong = Sub Wit
type family (a :: Maybe k) <|> (b :: Maybe k) :: Maybe k where
Nothing <|> a = a
a <|> Nothing = a
Just a <|> Just b = Just a
infixr 4 <|>
maybeAltCong :: (a ~ c,b ~ d) :- ((a <|> b) ~ (c <|> d))
maybeAltCong = Sub Wit
type family FromJust (m :: Maybe k) :: k where
FromJust (Just a) = a
fromJustCong :: (a ~ b) :- (FromJust a ~ FromJust b)
fromJustCong = Sub Wit
type instance Mempty = Nothing
type instance a <> b = a <|> b