Data.Default.Singletons

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.

Documentation

Optional Datatype

data Opt (def :: k) where

Optional type with either a Default promoted value def, or Some specific Demoted value.

Constructors

Def :: forall {k} def. SingDef def => Opt (def :: k)

Some :: forall {k} def. 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 :: forall {k} def. SingDef def => Maybe (Demote k) -> Opt (def :: 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"

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 :: forall {k} def m. 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

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

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 ...

Negate a Natural type .

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

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

type family z % n :: Q where ...

Construct a rational type in reduced form.

Equations

(Pos p) % q = Pos (Div p (GCD p q)) :% Div q (GCD p q)

(NegOneMinus p) % q = Neg (Div (1 + p) (GCD (1 + p) q)) :% Div q (GCD (1 + p) q)

type family Reduce q :: Q where ...

Perform reduction on a rational type, idempotently.

Reduce (Reduce q) ~ Reduce q

Equations

Reduce (z :% n) = z % n

type family GCD (a :: Natural) (b :: Natural) :: Natural where ...

Construct the greatest common divisor of Natural types.

Equations

GCD 0 0 = 1

GCD 0 b = b

GCD a 0 = a

GCD a b = GCD b (Mod a b)

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)