singletons-1.1: A framework for generating singleton types

Data.Singletons.Prelude.Ord

Contents

Description

Defines the promoted version of Ord, `POrd`, and the singleton version, `SOrd`.

Synopsis

# Documentation

class (PEq (KProxy :: KProxy a), kproxy ~ KProxy) => POrd kproxy Source

Associated Types

type Compare arg arg :: Ordering Source

type arg :< arg :: Bool Source

type arg :>= arg :: Bool Source

type arg :> arg :: Bool Source

type arg :<= arg :: Bool Source

type Max arg arg :: a Source

type Min arg arg :: a Source

Instances

 POrd Bool (KProxy Bool) POrd Ordering (KProxy Ordering) POrd Nat (KProxy Nat) POrd Symbol (KProxy Symbol) POrd () (KProxy ()) POrd [k] (KProxy [k]) POrd (Maybe k) (KProxy (Maybe k)) POrd (Either k k) (KProxy (Either k k)) POrd ((,) k k) (KProxy ((,) k k)) POrd ((,,) k k k) (KProxy ((,,) k k k)) POrd ((,,,) k k k k) (KProxy ((,,,) k k k k)) POrd ((,,,,) k k k k k) (KProxy ((,,,,) k k k k k)) POrd ((,,,,,) k k k k k k) (KProxy ((,,,,,) k k k k k k)) POrd ((,,,,,,) k k k k k k k) (KProxy ((,,,,,,) k k k k k k k))

class (kproxy ~ KProxy, SEq (KProxy :: KProxy a)) => SOrd kproxy where Source

Minimal complete definition

Nothing

Methods

sCompare :: forall x y. Sing x -> Sing y -> Sing (Compare x y) Source

(%:<) :: forall x y. Sing x -> Sing y -> Sing (x :< y) Source

(%:<=) :: forall x y. Sing x -> Sing y -> Sing (x :<= y) Source

(%:>) :: forall x y. Sing x -> Sing y -> Sing (x :> y) Source

(%:>=) :: forall x y. Sing x -> Sing y -> Sing (x :>= y) Source

sMax :: forall x y. Sing x -> Sing y -> Sing (Max x y) Source

sMin :: forall x y. Sing x -> Sing y -> Sing (Min x y) Source

`thenCmp` returns its second argument if its first is `EQ`; otherwise, it returns its first argument.

type family ThenCmp a a :: Ordering Source

Equations

 ThenCmp EQ x = x ThenCmp LT z = LTSym0 ThenCmp GT z = GTSym0

sThenCmp :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t) Source

data family Sing a Source

The singleton kind-indexed data family.

Instances

 TestCoercion * (Sing *) SDecide k (KProxy k) => TestEquality k (Sing k) data Sing Bool whereSFalse :: (~) Bool z False => Sing Bool zSTrue :: (~) Bool z True => Sing Bool z data Sing Ordering whereSLT :: (~) Ordering z LT => Sing Ordering zSEQ :: (~) Ordering z EQ => Sing Ordering zSGT :: (~) Ordering z GT => Sing Ordering z data Sing * whereSTypeRep :: Typeable * a => Sing * a data Sing Nat whereSNat :: KnownNat n => Sing Nat n data Sing Symbol whereSSym :: KnownSymbol n => Sing Symbol n data Sing () whereSTuple0 :: (~) () z () => Sing () z data Sing [a0] whereSNil :: (~) [a] z ([] a) => Sing [a] zSCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z data Sing (Maybe a0) whereSNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) zSJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z data Sing (TyFun k1 k2 -> *) = SLambda {applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t)} data Sing (Either a0 b0) whereSLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) zSRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z data Sing ((,) a0 b0) whereSTuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z data Sing ((,,) a0 b0 c0) whereSTuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z data Sing ((,,,) a0 b0 c0 d0) whereSTuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z data Sing ((,,,,) a0 b0 c0 d0 e0) whereSTuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) whereSTuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) whereSTuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> Sing ((,,,,,,) a b c d e f g) z

## Defunctionalization symbols

data ThenCmpSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun Ordering (TyFun Ordering Ordering -> *) -> *) ThenCmpSym0 type Apply (TyFun Ordering Ordering -> *) Ordering ThenCmpSym0 l0 = ThenCmpSym1 l0

data ThenCmpSym1 l l Source

Instances

 SuppressUnusedWarnings (Ordering -> TyFun Ordering Ordering -> *) ThenCmpSym1 type Apply Ordering Ordering (ThenCmpSym1 l1) l0 = ThenCmpSym2 l1 l0

type ThenCmpSym2 t t = ThenCmp t t Source

data CompareSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k Ordering -> *) -> *) (CompareSym0 k) type Apply (TyFun k Ordering -> *) k (CompareSym0 k) l0 = CompareSym1 k l0

data CompareSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k Ordering -> *) (CompareSym1 k) type Apply Ordering k (CompareSym1 k l1) l0 = CompareSym2 k l1 l0

type CompareSym2 t t = Compare t t Source

data (:<\$) l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k Bool -> *) -> *) ((:<\$) k) type Apply (TyFun k Bool -> *) k ((:<\$) k) l0 = (:<\$\$) k l0

data l :<\$\$ l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:<\$\$) k) type Apply Bool k ((:<\$\$) k l1) l0 = (:<\$\$\$) k l1 l0

type (:<\$\$\$) t t = (:<) t t Source

data (:<=\$) l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k Bool -> *) -> *) ((:<=\$) k) type Apply (TyFun k Bool -> *) k ((:<=\$) k) l0 = (:<=\$\$) k l0

data l :<=\$\$ l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:<=\$\$) k) type Apply Bool k ((:<=\$\$) k l1) l0 = (:<=\$\$\$) k l1 l0

type (:<=\$\$\$) t t = (:<=) t t Source

data (:>\$) l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k Bool -> *) -> *) ((:>\$) k) type Apply (TyFun k Bool -> *) k ((:>\$) k) l0 = (:>\$\$) k l0

data l :>\$\$ l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:>\$\$) k) type Apply Bool k ((:>\$\$) k l1) l0 = (:>\$\$\$) k l1 l0

type (:>\$\$\$) t t = (:>) t t Source

data (:>=\$) l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k Bool -> *) -> *) ((:>=\$) k) type Apply (TyFun k Bool -> *) k ((:>=\$) k) l0 = (:>=\$\$) k l0

data l :>=\$\$ l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:>=\$\$) k) type Apply Bool k ((:>=\$\$) k l1) l0 = (:>=\$\$\$) k l1 l0

type (:>=\$\$\$) t t = (:>=) t t Source

data MaxSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (MaxSym0 k) type Apply (TyFun k k -> *) k (MaxSym0 k) l0 = MaxSym1 k l0

data MaxSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k k -> *) (MaxSym1 k) type Apply k k (MaxSym1 k l1) l0 = MaxSym2 k l1 l0

type MaxSym2 t t = Max t t Source

data MinSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (MinSym0 k) type Apply (TyFun k k -> *) k (MinSym0 k) l0 = MinSym1 k l0

data MinSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k k -> *) (MinSym1 k) type Apply k k (MinSym1 k l1) l0 = MinSym2 k l1 l0

type MinSym2 t t = Min t t Source