singletons-2.1: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

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 infix 4 Source

type arg :<= arg :: Bool infix 4 Source

type arg :> arg :: Bool infix 4 Source

type arg :>= arg :: Bool infix 4 Source

type Max arg arg :: a Source

type Min arg arg :: a Source

Instances

POrd Bool (KProxy Bool) Source 
POrd Ordering (KProxy Ordering) Source 
POrd () (KProxy ()) Source 
POrd [a] (KProxy [a]) Source 
POrd (Maybe a) (KProxy (Maybe a)) Source 
POrd (Either a b) (KProxy (Either a b)) Source 
POrd ((,) a b) (KProxy ((,) a b)) Source 
POrd ((,,) a b c) (KProxy ((,,) a b c)) Source 
POrd ((,,,) a b c d) (KProxy ((,,,) a b c d)) Source 
POrd ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) Source 
POrd ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) Source 
POrd ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) Source 

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

Minimal complete definition

Nothing

Methods

sCompare :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) Source

(%:<) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<$) t) t :: Bool) infix 4 Source

(%:<=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<=$) t) t :: Bool) infix 4 Source

(%:>) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:>$) t) t :: Bool) infix 4 Source

(%:>=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:>=$) t) t :: Bool) infix 4 Source

sMax :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) Source

sMin :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) Source

Instances

SOrd Bool (KProxy Bool) Source 
SOrd Ordering (KProxy Ordering) Source 
SOrd () (KProxy ()) Source 
(SOrd a0 (KProxy a0), SOrd [a0] (KProxy [a0])) => SOrd [a] (KProxy [a]) Source 
SOrd a0 (KProxy a0) => SOrd (Maybe a) (KProxy (Maybe a)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0)) => SOrd (Either a b) (KProxy (Either a b)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0)) => SOrd ((,) a b) (KProxy ((,) a b)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0)) => SOrd ((,,) a b c) (KProxy ((,,) a b c)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0)) => SOrd ((,,,) a b c d) (KProxy ((,,,) a b c d)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0), SOrd e0 (KProxy e0)) => SOrd ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0), SOrd e0 (KProxy e0), SOrd f0 (KProxy f0)) => SOrd ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) Source 
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0), SOrd e0 (KProxy e0), SOrd f0 (KProxy f0), SOrd g0 (KProxy g0)) => SOrd ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) 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_1627669159 = LTSym0 
ThenCmp GT _z_1627669162 = GTSym0 

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

data family Sing a Source

The singleton kind-indexed data family.

Instances

data Sing Bool where Source 
data Sing Ordering where Source 
data Sing * where Source 
data Sing Nat where Source 
data Sing Symbol where Source 
data Sing () where Source 
data Sing [a0] where Source 
data Sing (Maybe a0) where Source 
data Sing (TyFun k1 k2 -> *) = SLambda {} Source 
data Sing (Either a0 b0) where Source 
data Sing ((,) a0 b0) where Source 
data Sing ((,,) a0 b0 c0) where Source 
data Sing ((,,,) a0 b0 c0 d0) where Source 
data Sing ((,,,,) a0 b0 c0 d0 e0) where Source 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where Source 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where Source 

Defunctionalization symbols

type ThenCmpSym2 t t = ThenCmp t t Source

data CompareSym0 l Source

Instances

data CompareSym1 l l Source

Instances

type CompareSym2 t t = Compare t t Source

data (:<$) l Source

Instances

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

data l :<$$ l Source

Instances

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

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

data (:<=$) l Source

Instances

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

data l :<=$$ l Source

Instances

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

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

data (:>$) l Source

Instances

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

data l :>$$ l Source

Instances

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

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

data (:>=$) l Source

Instances

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

data l :>=$$ l Source

Instances

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

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

data MaxSym0 l Source

Instances

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

data MaxSym1 l l Source

Instances

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

type MaxSym2 t t = Max t t Source

data MinSym0 l Source

Instances

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

data MinSym1 l l Source

Instances

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

type MinSym2 t t = Min t t Source