Data.Default.Singletons

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 (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"

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)

Documentation

Optional Datatype

data Opt (def :: k) where

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

Constructors

Def :: SingDef def => Opt (def :: k)

Some :: Demote k -> Opt (def :: k)

Instances

IsString (Demote k) => IsString (Opt def)

Defined in Data.Default.Singletons

Methods

fromString :: String -> Opt def

SingDef def => Monoid (Opt def)

Defined in Data.Default.Singletons

Methods

mempty :: Opt def

mappend :: Opt def -> Opt def -> Opt def

mconcat :: [Opt def] -> Opt def

Semigroup (Opt def)

Defined in Data.Default.Singletons

Methods

(<>) :: Opt def -> Opt def -> Opt def

sconcat :: NonEmpty (Opt def) -> Opt def

stimes :: Integral b => b -> Opt def -> Opt def

IsList (Demote k) => IsList (Opt def)

Defined in Data.Default.Singletons

Associated Types

type Item (Opt def)

Methods

fromList :: [Item (Opt def)] -> Opt def

fromListN :: Int -> [Item (Opt def)] -> Opt def

toList :: Opt def -> [Item (Opt def)]

Num (Demote k) => Num (Opt def)

Defined in Data.Default.Singletons

Methods

(+) :: Opt def -> Opt def -> Opt def

(-) :: Opt def -> Opt def -> Opt def

(*) :: Opt def -> Opt def -> Opt def

negate :: Opt def -> Opt def

abs :: Opt def -> Opt def

signum :: Opt def -> Opt def

fromInteger :: Integer -> Opt def

(SingDef def, Read (Demote k)) => Read (Opt def)

Defined in Data.Default.Singletons

Methods

readsPrec :: Int -> ReadS (Opt def)

readList :: ReadS [Opt def]

readPrec :: ReadPrec (Opt def)

readListPrec :: ReadPrec [Opt def]

Fractional (Demote k) => Fractional (Opt def)

Defined in Data.Default.Singletons

Methods

(/) :: Opt def -> Opt def -> Opt def

recip :: Opt def -> Opt def

fromRational :: Rational -> Opt def

(SingDef def, Show (Demote k)) => Show (Opt def)

Defined in Data.Default.Singletons

Methods

showsPrec :: Int -> Opt def -> ShowS

show :: Opt def -> String

showList :: [Opt def] -> ShowS

SingDef def => Default (Opt def)

Defined in Data.Default.Singletons

Methods

def :: Opt def

(SingDef def, Eq (Demote k)) => Eq (Opt def)

Defined in Data.Default.Singletons

Methods

(==) :: Opt def -> Opt def -> Bool

(/=) :: Opt def -> Opt def -> Bool

(SingDef def, Ord (Demote k)) => Ord (Opt def)

Defined in Data.Default.Singletons

Methods

compare :: Opt def -> Opt def -> Ordering

(<) :: Opt def -> Opt def -> Bool

(<=) :: Opt def -> Opt def -> Bool

(>) :: Opt def -> Opt def -> Bool

(>=) :: Opt def -> Opt def -> Bool

max :: Opt def -> Opt def -> Opt def

min :: Opt def -> Opt def -> Opt def

type Item (Opt def)

Defined in Data.Default.Singletons

type Item (Opt def) = Item (Demote k)

type SingDef (def :: k) = (SingI def, SingKind k)

Constraint required to demote @def.

optionally :: SingDef def => Maybe (Demote k) -> Opt (def :: k)

Constructs an Opt from a Maybe. Nothing maps to Def, and Just maps to Some.

definite :: forall k def. Opt (def :: k) -> Demote k

Deconstructs an Opt to a Demoted value. Def maps to demote @def, and Some maps to its argument.

perhaps :: Alternative m => Opt (def :: k) -> m (Demote k)

Deconstructs an Opt to an Alternative Demoted value. Def maps to empty, and Some maps to pure, inverting optionally.

Promoted Datakinds

data Z

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

Constructors

Pos Natural

NegOneMinus Natural

Instances

Enum Z

Defined in Data.Default.Singletons

Methods

succ :: Z -> Z

pred :: Z -> Z

toEnum :: Int -> Z

fromEnum :: Z -> Int

enumFrom :: Z -> [Z]

enumFromThen :: Z -> Z -> [Z]

enumFromTo :: Z -> Z -> [Z]

enumFromThenTo :: Z -> Z -> Z -> [Z]

Num Z

Defined in Data.Default.Singletons

Methods

(+) :: Z -> Z -> Z

(-) :: Z -> Z -> Z

(*) :: Z -> Z -> Z

negate :: Z -> Z

abs :: Z -> Z

signum :: Z -> Z

fromInteger :: Integer -> Z

Read Z

Defined in Data.Default.Singletons

Methods

readsPrec :: Int -> ReadS Z

readList :: ReadS [Z]

readPrec :: ReadPrec Z

readListPrec :: ReadPrec [Z]

Integral Z

Defined in Data.Default.Singletons

Methods

quot :: Z -> Z -> Z

rem :: Z -> Z -> Z

div :: Z -> Z -> Z

mod :: Z -> Z -> Z

quotRem :: Z -> Z -> (Z, Z)

divMod :: Z -> Z -> (Z, Z)

toInteger :: Z -> Integer

Real Z

Defined in Data.Default.Singletons

Methods

toRational :: Z -> Rational

Show Z

Defined in Data.Default.Singletons

Methods

showsPrec :: Int -> Z -> ShowS

show :: Z -> String

showList :: [Z] -> ShowS

Eq Z

Defined in Data.Default.Singletons

Methods

(==) :: Z -> Z -> Bool

(/=) :: Z -> Z -> Bool

Ord Z

Defined in Data.Default.Singletons

Methods

compare :: Z -> Z -> Ordering

(<) :: Z -> Z -> Bool

(<=) :: Z -> Z -> Bool

(>) :: Z -> Z -> Bool

(>=) :: Z -> Z -> Bool

max :: Z -> Z -> Z

min :: Z -> Z -> Z

SingKind Z

Defined in Data.Default.Singletons

Associated Types

type Demote Z = (r :: Type)

Methods

fromSing :: forall (a :: Z). Sing a -> Demote Z

toSing :: Demote Z -> SomeSing Z

KnownNat n => SingI ('NegOneMinus n :: Z)

Defined in Data.Default.Singletons

Methods

sing :: Sing ('NegOneMinus n)

KnownNat n => SingI ('Pos n :: Z)

Defined in Data.Default.Singletons

Methods

sing :: Sing ('Pos n)

type Demote Z

Defined in Data.Default.Singletons

type Demote Z = Integer

type Sing

Defined in Data.Default.Singletons

type Sing = SInteger

type family Neg n where ...

Type family for negating a Natural.

Equations

Neg 0 = Pos 0

Neg n = NegOneMinus (n - 1)

data Q

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

Constructors

(:%) Z Natural

Instances

Num Q

Defined in Data.Default.Singletons

Methods

(+) :: Q -> Q -> Q

(-) :: Q -> Q -> Q

(*) :: Q -> Q -> Q

negate :: Q -> Q

abs :: Q -> Q

signum :: Q -> Q

fromInteger :: Integer -> Q

Read Q

Defined in Data.Default.Singletons

Methods

readsPrec :: Int -> ReadS Q

readList :: ReadS [Q]

readPrec :: ReadPrec Q

readListPrec :: ReadPrec [Q]

Fractional Q

Defined in Data.Default.Singletons

Methods

(/) :: Q -> Q -> Q

recip :: Q -> Q

fromRational :: Rational -> Q

Real Q

Defined in Data.Default.Singletons

Methods

toRational :: Q -> Rational

Show Q

Defined in Data.Default.Singletons

Methods

showsPrec :: Int -> Q -> ShowS

show :: Q -> String

showList :: [Q] -> ShowS

Eq Q

Defined in Data.Default.Singletons

Methods

(==) :: Q -> Q -> Bool

(/=) :: Q -> Q -> Bool

Ord Q

Defined in Data.Default.Singletons

Methods

compare :: Q -> Q -> Ordering

(<) :: Q -> Q -> Bool

(<=) :: Q -> Q -> Bool

(>) :: Q -> Q -> Bool

(>=) :: Q -> Q -> Bool

max :: Q -> Q -> Q

min :: Q -> Q -> Q

SingKind Q

Defined in Data.Default.Singletons

Associated Types

type Demote Q = (r :: Type)

Methods

fromSing :: forall (a :: Q). Sing a -> Demote Q

toSing :: Demote Q -> SomeSing Q

(SingI num, SingI denom) => SingI (num ':% denom :: Q)

Defined in Data.Default.Singletons

Methods

sing :: Sing (num ':% denom)

type Demote Q

Defined in Data.Default.Singletons

type Demote Q = Rational

type Sing

Defined in Data.Default.Singletons

type Sing = SRational

data SInteger (n :: Z) where

Singleton representation for the Z kind.

Constructors

SPos :: SNat n -> SInteger (Pos n)

SNegOneMinus :: SNat n -> SInteger (NegOneMinus n)

data SRational (n :: Q) where

Singleton representation for the Q kind.

Constructors

SRational :: SInteger n -> SNat m -> SRational (n :% m)

Reexport Demote

demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k

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)

type family Demote k = (r :: Type) | r -> 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.

Instances

type Demote All

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote All = All

type Demote Any

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote Any = Any

type Demote Void

Defined in Data.Singletons.Base.Instances

type Demote Void = Void

type Demote Ordering

Defined in Data.Singletons.Base.Instances

type Demote Ordering = Ordering

type Demote Q

Defined in Data.Default.Singletons

type Demote Q = Rational

type Demote Z

Defined in Data.Default.Singletons

type Demote Z = Integer

type Demote Natural

Defined in GHC.TypeLits.Singletons.Internal

type Demote Natural = Natural

type Demote ()

Defined in Data.Singletons.Base.Instances

type Demote () = ()

type Demote Bool

Defined in Data.Singletons.Base.Instances

type Demote Bool = Bool

type Demote Char

Defined in GHC.TypeLits.Singletons.Internal

type Demote Char = Char

type Demote Symbol

Defined in GHC.TypeLits.Singletons.Internal

type Demote Symbol = Text

type Demote (Identity a)

Defined in Data.Singletons.Base.Instances

type Demote (Identity a) = Identity (Demote a)

type Demote (First a)

Defined in Data.Monoid.Singletons

type Demote (First a) = First (Demote a)

type Demote (Last a)

Defined in Data.Monoid.Singletons

type Demote (Last a) = Last (Demote a)

type Demote (Down a)

Defined in Data.Ord.Singletons

type Demote (Down a) = Down (Demote a)

type Demote (First a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (First a) = First (Demote a)

type Demote (Last a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (Last a) = Last (Demote a)

type Demote (Max a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (Max a) = Max (Demote a)

type Demote (Min a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (Min a) = Min (Demote a)

type Demote (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (WrappedMonoid m) = WrappedMonoid (Demote m)

type Demote (Dual a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (Dual a) = Dual (Demote a)

type Demote (Product a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (Product a) = Product (Demote a)

type Demote (Sum a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Demote (Sum a) = Sum (Demote a)

type Demote (NonEmpty a)

Defined in Data.Singletons.Base.Instances

type Demote (NonEmpty a) = NonEmpty (Demote a)

type Demote (MaxInternal a)

Defined in Data.Foldable.Singletons

type Demote (MaxInternal a) = MaxInternal (Demote a)

type Demote (MinInternal a)

Defined in Data.Foldable.Singletons

type Demote (MinInternal a) = MinInternal (Demote a)

type Demote (Maybe a)

Defined in Data.Singletons.Base.Instances

type Demote (Maybe a) = Maybe (Demote a)

type Demote [a]

Defined in Data.Singletons.Base.Instances

type Demote [a] = [Demote a]

type Demote (Either a b)

Defined in Data.Singletons.Base.Instances

type Demote (Either a b) = Either (Demote a) (Demote b)

type Demote (Proxy t)

Defined in Data.Proxy.Singletons

type Demote (Proxy t) = Proxy t

type Demote (Arg a b)

Defined in Data.Semigroup.Singletons

type Demote (Arg a b) = Arg (Demote a) (Demote b)

type Demote (WrappedSing a)

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

type Demote (k1 ~> k2)

Defined in Data.Singletons

type Demote (k1 ~> k2) = Demote k1 -> Demote k2

type Demote (a, b)

Defined in Data.Singletons.Base.Instances

type Demote (a, b) = (Demote a, Demote b)

type Demote (Const a b)

Defined in Data.Functor.Const.Singletons

type Demote (Const a b) = Const (Demote a) b

type Demote (a, b, c)

Defined in Data.Singletons.Base.Instances

type Demote (a, b, c) = (Demote a, Demote b, Demote c)

type Demote (a, b, c, d)

Defined in Data.Singletons.Base.Instances

type Demote (a, b, c, d) = (Demote a, Demote b, Demote c, Demote d)

type Demote (a, b, c, d, e)

Defined in Data.Singletons.Base.Instances

type Demote (a, b, c, d, e) = (Demote a, Demote b, Demote c, Demote d, Demote e)

type Demote (a, b, c, d, e, f)

Defined in Data.Singletons.Base.Instances

type Demote (a, b, c, d, e, f) = (Demote a, Demote b, Demote c, Demote d, Demote e, Demote f)

type Demote (a, b, c, d, e, f, g)

Defined in Data.Singletons.Base.Instances

type Demote (a, b, c, d, e, f, g) = (Demote a, Demote b, Demote c, Demote d, Demote e, Demote f, Demote g)