Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Ord

Contents

Defunctionalization symbols

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.

thenCmp :: Ordering -> Ordering -> Ordering Source

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 where SFalse :: (~) Bool z False => Sing Bool z STrue :: (~) Bool z True => Sing Bool z
data Sing Ordering where SLT :: (~) Ordering z LT => Sing Ordering z SEQ :: (~) Ordering z EQ => Sing Ordering z SGT :: (~) Ordering z GT => Sing Ordering z
data Sing * where STypeRep :: Typeable * a => Sing * a
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z () => Sing () z
data Sing [a0] where SNil :: (~) [a] z ([] a) => Sing [a] z SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z
data Sing (Maybe a0) where SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z SJust :: (~) (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) where SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) 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) where STuple4 :: (~) ((,,,) 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) where STuple5 :: (~) ((,,,,) 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) where STuple6 :: (~) ((,,,,,) 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) where STuple7 :: (~) ((,,,,,,) 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

type LTSym0 = LT Source

type EQSym0 = EQ Source

type GTSym0 = GT 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