-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | An optional type with type level default
--
-- dependently typed optional values with default
@package singletons-default
@version 0.1.0.2
-- | This module defines an Optional type with either a
-- Default promoted value, or Some specific demoted value.
--
--
-- >>> definite (Def :: Opt True)
-- True
--
-- >>> definite (Some False :: Opt True)
-- False
--
-- >>> definite (Some True :: Opt True)
-- True
--
-- >>> maybe "def" show (perhaps (Def :: Opt True))
-- "def"
--
-- >>> maybe "def" show (perhaps (Some True :: Opt True))
-- "True"
--
-- >>> maybe "def" show (perhaps (Some False :: Opt True))
-- "False"
--
--
-- Promoted datakinds and their Demoted datatypes include:
--
--
-- >>> :kind! Demote Symbol
-- Demote Symbol :: *
-- = Text
--
-- >>> :kind! Demote Natural
-- Demote Natural :: *
-- = Natural
--
-- >>> :kind! Demote Char
-- Demote Char :: *
-- = Char
--
-- >>> :kind! Demote Bool
-- Demote Bool :: *
-- = Bool
--
-- >>> :kind! Demote [k]
-- Demote [k] :: *
-- = [Demote k]
--
-- >>> :kind! Demote String
-- Demote String :: *
-- = [Char]
--
-- >>> :kind! Demote (Either k j)
-- Demote (Either k j) :: *
-- = Either (Demote k) (Demote j)
--
-- >>> :kind! Demote (k,j)
-- Demote (k,j) :: *
-- = (Demote k, Demote j)
--
--
-- Because there is no promoted Integer and Rational
-- datakinds, this module defines them as Z and Q.
--
--
-- >>> :kind! Demote Z
-- Demote Z :: *
-- = Integer
--
-- >>> :kind! Demote Q
-- Demote Q :: *
-- = Ratio Integer
--
--
-- The Opt type comes with Num, Integral,
-- Fractional, and Real instances, using definite
-- values to do arithmetic; and IsString and IsList
-- instances, which let you use literals to construct Opt.
--
--
-- >>> "text" :: Opt ("hello" :: Symbol)
-- Some "text"
--
-- >>> "string" :: Opt (['a','b','c'] :: String)
-- Some "string"
--
-- >>> [1, 2] :: Opt ('[] :: [Natural])
-- Some [1,2]
--
-- >>> Def + 0 :: Opt (Pos 1 :: Z)
-- Some 1
--
-- >>> 0.5 + Def :: Opt (Neg 1 :% 3 :: Q)
-- Some (1 % 6)
--
module Data.Default.Singletons
-- | Optional type with either a Default promoted value
-- def, or Some specific Demoted value.
--
-- Opt is a Monoid which yields the leftmost Some.
--
--
-- >>> mempty :: Opt "xyz"
-- Def
--
-- >>> Def <> "abc" <> "qrs" :: Opt "xyz"
-- Some "abc"
--
--
-- You can use Opt as an optional function argument.
--
--
-- >>> let greet (name :: Opt "Anon") = "Welcome, " <> definite name <> "."
--
-- >>> greet "Sarah"
-- "Welcome, Sarah."
--
-- >>> greet Def
-- "Welcome, Anon."
--
--
-- Or, you can use Opt as an optional field in your record type.
--
--
-- >>> :{
-- data Person = Person
-- { name :: Text
-- , age :: Natural
-- , alive :: Opt (True :: Bool)
-- }
-- :}
--
-- >>> let isAlive person = definite (alive person)
--
-- >>> let jim = Person {name = "Jim", age = 40, alive = Def}
--
-- >>> isAlive jim
-- True
--
data Opt (def :: k)
[Def] :: SingDef def => Opt (def :: k)
[Some] :: SingDef def => Demote k -> Opt (def :: k)
-- | Constraint required to demote @def.
type SingDef (def :: k) = (SingI def, SingKind k)
-- | Constructs an Opt from a Maybe. Nothing maps to
-- Def, and Just maps to Some.
optionally :: SingDef def => Maybe (Demote k) -> Opt (def :: k)
-- | Deconstructs an Opt to a Demoted value. Def maps
-- to demote @def, and Some maps to its argument.
definite :: forall k def. Opt (def :: k) -> Demote k
-- | Deconstructs an Opt to an Alternative Demoted
-- value. Def maps to empty, and Some maps to
-- pure, inverting optionally.
perhaps :: Alternative m => Opt (def :: k) -> m (Demote k)
-- | Datakind Z, promoting Integer,
--
--
-- >>> :kind! Demote Z
-- Demote Z :: *
-- = Integer
--
--
-- with Pos for constructing nonnegative integer types, and
-- Neg for constructing nonpositive integer types.
--
--
-- >>> demote @(Pos 90210)
-- 90210
--
-- >>> demote @(Neg 5)
-- -5
--
-- >>> demote @(Neg 0)
-- 0
--
-- >>> demote @(Pos 0)
-- 0
--
data Z
Pos :: Natural -> Z
NegOneMinus :: Natural -> Z
-- | Type family for negating a Natural.
type family Neg n
-- | Datakind Q, promoting Rational,
--
--
-- >>> :kind! Demote Q
-- Demote Q :: *
-- = Ratio Integer
--
--
-- with :% for constructing rational types.
--
--
-- >>> demote @(Pos 7 :% 11)
-- 7 % 11
--
-- >>> demote @(Neg 4 :% 2)
-- (-2) % 1
--
data Q
(:%) :: Z -> Natural -> Q
-- | Singleton representation for the Z kind.
data SInteger (n :: Z)
[SPos] :: SNat n -> SInteger (Pos n)
[SNegOneMinus] :: SNat n -> SInteger (NegOneMinus n)
-- | Singleton representation for the Q kind.
data SRational (n :: Q)
[SRational] :: SInteger n -> SNat m -> SRational (n :% m)
-- | A convenience function that takes a type as input and demotes it to
-- its value-level counterpart as output. This uses SingKind and
-- SingI behind the scenes, so demote = fromSing
-- sing.
--
-- This function is intended to be used with TypeApplications.
-- For example:
--
--
-- >>> demote @True
-- True
--
--
--
-- >>> demote @(Nothing :: Maybe Ordering)
-- Nothing
--
--
--
-- >>> demote @(Just EQ)
-- Just EQ
--
--
--
-- >>> demote @'(True,EQ)
-- (True,EQ)
--
demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k
-- | Get a base type from the promoted kind. For example, Demote
-- Bool will be the type Bool. Rarely, the type and kind do
-- not match. For example, Demote Nat is Natural.
type family Demote k = (r :: Type) | r -> k
instance GHC.Show.Show Data.Default.Singletons.Z
instance GHC.Read.Read Data.Default.Singletons.Z
instance GHC.Classes.Ord Data.Default.Singletons.Z
instance GHC.Classes.Eq Data.Default.Singletons.Z
instance GHC.Read.Read Data.Default.Singletons.Q
instance GHC.Show.Show Data.Default.Singletons.Q
instance GHC.Classes.Ord Data.Default.Singletons.Q
instance GHC.Classes.Eq Data.Default.Singletons.Q
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.Show.Show (Data.Singletons.Demote k)) => GHC.Show.Show (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.Read.Read (Data.Singletons.Demote k)) => GHC.Read.Read (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.Classes.Eq (Data.Singletons.Demote k)) => GHC.Classes.Eq (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.Classes.Ord (Data.Singletons.Demote k)) => GHC.Classes.Ord (Data.Default.Singletons.Opt def)
instance Data.Singletons.SingKind Data.Default.Singletons.Q
instance (Data.Singletons.SingI num, Data.Singletons.SingI denom) => Data.Singletons.SingI (num 'Data.Default.Singletons.:% denom)
instance GHC.Real.Real Data.Default.Singletons.Q
instance GHC.Real.Fractional Data.Default.Singletons.Q
instance GHC.Num.Num Data.Default.Singletons.Q
instance Data.Singletons.SingKind Data.Default.Singletons.Z
instance GHC.TypeNats.KnownNat n => Data.Singletons.SingI ('Data.Default.Singletons.Pos n)
instance GHC.TypeNats.KnownNat n => Data.Singletons.SingI ('Data.Default.Singletons.NegOneMinus n)
instance GHC.Real.Real Data.Default.Singletons.Z
instance GHC.Real.Integral Data.Default.Singletons.Z
instance GHC.Enum.Enum Data.Default.Singletons.Z
instance GHC.Num.Num Data.Default.Singletons.Z
instance forall k (def :: k). GHC.Base.Semigroup (Data.Default.Singletons.Opt def)
instance forall k (def :: k). Data.Default.Singletons.SingDef def => GHC.Base.Monoid (Data.Default.Singletons.Opt def)
instance forall k (def :: k). Data.Default.Singletons.SingDef def => Data.Default.Class.Default (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.Num.Num (Data.Singletons.Demote k)) => GHC.Num.Num (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.Real.Fractional (Data.Singletons.Demote k)) => GHC.Real.Fractional (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, Data.String.IsString (Data.Singletons.Demote k)) => Data.String.IsString (Data.Default.Singletons.Opt def)
instance forall k (def :: k). (Data.Default.Singletons.SingDef def, GHC.IsList.IsList (Data.Singletons.Demote k)) => GHC.IsList.IsList (Data.Default.Singletons.Opt def)