Type.Family.Maybe

Convenient type families for working with type-level Maybes.

Documentation

type family MaybeC (mc :: Maybe Constraint) :: Constraint where ...

Take a Maybe Constraint to a Constraint.

Equations

MaybeC Nothing = ØC

MaybeC (Just c) = c

type family IsNothing (a :: Maybe k) :: Bool where ...

Equations

IsNothing Nothing = True

IsNothing (Just a) = False

nothingCong :: (a ~ b) :- (IsNothing a ~ IsNothing b)

nothingNotJust :: (Nothing ~ Just a) :- Fail

type family (f :: k -> l) <$> (a :: Maybe k) :: Maybe l where ... infixr 4

Map over a type-level Maybe.

Equations

f <$> Nothing = Nothing

f <$> (Just a) = Just (f a)

maybeFmapCong :: (f ~ g, a ~ b) :- ((f <$> a) ~ (g <$> b))

type family (f :: Maybe (k -> l)) <&> (a :: k) :: Maybe l where ... infixl 5

Equations

Nothing <&> a = Nothing

(Just f) <&> a = Just (f a)

maybePamfCong :: (f ~ g, a ~ b) :- ((f <&> a) ~ (g <&> b))

type family (f :: Maybe (k -> l)) <*> (a :: Maybe k) :: Maybe l where ... infixr 4

Equations

Nothing <*> a = Nothing

f <*> Nothing = Nothing

(Just f) <*> (Just a) = Just (f a)

maybeApCong :: (f ~ g, a ~ b) :- ((f <*> a) ~ (g <*> b))

type family (a :: Maybe k) <|> (b :: Maybe k) :: Maybe k where ... infixr 4

Equations

Nothing <|> a = a

a <|> Nothing = a

(Just a) <|> (Just b) = Just a

maybeAltCong :: (a ~ c, b ~ d) :- ((a <|> b) ~ (c <|> d))

type family FromJust (m :: Maybe k) :: k where ...

Equations

FromJust (Just a) = a

fromJustCong :: (a ~ b) :- (FromJust a ~ FromJust b)