-- 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.7 -- | This module defines an Optional type with either a -- Default promoted value type, or Some specific demoted -- value term. -- -- 
--   >>> definite (Def :: Opt True)
--   True
--   
--   >>> definite (Some False :: Opt (def :: Bool))
--   False
--   
--   >>> definite (Some True :: Opt False)
--   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"
--
-- -- The correspondence between promoted datakinds and demoted datatypes is -- inexact. Usually, Demote t ~ t, but not always such -- as: -- -- 
--   >>> :kind! Demote Symbol
--   Demote Symbol :: *
--   = Text
--
-- -- Because there is no promoted Integer and Rational -- datakinds in base, 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, which let you use literals and arithmetic to -- construct Some specific Opt value; -- -- 
--   >>> 4 :: Opt 20
--   Some 4
--   
--   >>> (Def + 0) * 1 :: Opt (Pos 8 :: Z)
--   Some 8
--   
--   >>> 0.5 + Def :: Opt (Neg 1 % 3 :: Q)
--   Some (1 % 6)
--
-- -- and IsString and IsList instances. -- -- 
--   >>> "text" :: Opt ("abc" :: Symbol)
--   Some "text"
--   
--   >>> "string" :: Opt (['a','b','c'] :: String)
--   Some "string"
--   
--   >>> [[1, 2],[3,4]] :: Opt ('[] :: [[Natural]])
--   Some [[1, 2],[3,4]]
--
-- -- Opt is a Monoid which yields the leftmost specific value -- when there are Some, and the Default value when there -- are none. -- -- 
--   >>> definite (mempty :: Opt "xyz")
--   "xyz"
--   
--   >>> definite (Def <> "abc" <> "qrs" <> Def :: Opt "xyz")
--   "abc"
--
-- -- You can use Opt as an optional function argument. -- -- 
--   >>> :{
--   greet :: Opt "Anon" -> Text
--   greet name = "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
--
-- -- You almost never need to include the datakind in your type signatures -- since it's usually inferrable from def. module Data.Default.Singletons -- | Optional type with either a Default promoted value -- def, or Some specific Demoted value. data Opt (def :: k) [Def] :: forall {k} def. SingDef def => Opt (def :: k) [Some] :: forall {k} 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. -- -- 
--   >>> definite (optionally @'[ '[1,2],'[3]] Nothing)
--   [[1,2],[3]]
--   
--   >>> definite (optionally @"foo" (Just "bar"))
--   "bar"
--
optionally :: forall {k} def. 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 :: forall {k} def m. 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
--
-- -- NonNegative integer types are matched cardinally by Pos, -- -- 
--   >>> :kind! Pos 9
--   Pos 9 :: Z
--   = Pos 9
--   
--   >>> :kind! Neg 0
--   Neg 0 :: Z
--   = Pos 0
--
-- -- and Negative integer types are matched ordinally by -- NegOneMinus. -- -- 
--   >>> :kind! Neg 6
--   Neg 6 :: Z
--   = NegOneMinus 5
--   
--   >>> :kind! Neg 1
--   Neg 1 :: Z
--   = NegOneMinus 0
--
data Z Pos :: Natural -> Z NegOneMinus :: Natural -> Z -- | Negate a Natural type . type family Neg n -- | Datakind Q, promoting Rational, -- -- 
--   >>> :kind! Demote Q
--   Demote Q :: *
--   = Ratio Integer
--
-- -- with :% for constructing (unreduced) and matching rational -- types, -- -- 
--   >>> demote @(Pos 7 :% 11)
--   7 % 11
--   
--   >>> demote @(Neg 4 :% 6)
--   (-2) % 3
--   
--   >>> :kind Pos 10 :% 10
--   Pos 10 :% 10 :: Q
--
-- -- and % and Reduce for constructing reduced rational -- types. -- -- 
--   >>> :kind! Pos 14 % 49
--   Pos 14 % 49 :: Q
--   = Pos 2 :% 7
--   
--   >>> type Percent n = Pos n :% 100
--   
--   >>> :kind! Percent 10
--   Percent 10 :: Q
--   = Pos 10 :% 100
--   
--   >>> :kind! Reduce (Percent 10)
--   Reduce (Percent 10) :: Q
--   = Pos 1 :% 10
--
data Q (:%) :: Z -> Natural -> Q -- | Construct a rational type in reduced form. type family (%) z n :: Q -- | Perform reduction on a rational type, idempotently. -- -- 
--   Reduce (Reduce q) ~ Reduce q
--
type family Reduce q :: Q -- | Construct the greatest common divisor of Natural types. type family GCD (a :: Natural) (b :: Natural) :: Natural -- | 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). GHC.Num.Num (Data.Singletons.Demote k) => GHC.Num.Num (Data.Default.Singletons.Opt def) instance forall k (def :: k). GHC.Real.Fractional (Data.Singletons.Demote k) => GHC.Real.Fractional (Data.Default.Singletons.Opt def) instance forall k (def :: k). Data.String.IsString (Data.Singletons.Demote k) => Data.String.IsString (Data.Default.Singletons.Opt def) instance forall k (def :: k). GHC.IsList.IsList (Data.Singletons.Demote k) => GHC.IsList.IsList (Data.Default.Singletons.Opt def)