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

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 :: SingDef def => Demote k -> Opt (def :: k)

Instances

(SingDef def, 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

(SingDef 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)]

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

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

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)

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)