first-class-families-0.8.1.0: First-class type families

Safe Haskell | Safe-Inferred
Language | Haskell2010

Fcf.Class.Ord

Contents

- Order
- Equality

Description

Equality and ordering.

Note that equality doesn't really require a class, it can be defined uniformly as `TyEq`.

Synopsis

- data Compare :: a -> a -> Exp Ordering
- data (<=) :: a -> a -> Exp Bool
- data (>=) :: a -> a -> Exp Bool
- data (<) :: a -> a -> Exp Bool
- data (>) :: a -> a -> Exp Bool
- data TyEq :: a -> b -> Exp Bool

# Order

data Compare :: a -> a -> Exp Ordering Source #

Type-level `compare` for totally ordered data types.

### Example

Expand

    >>> :kind! Eval (Compare "a" "b")
    Eval (Compare "a" "b") :: Ordering
    = LT

    >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])
    Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering
    = EQ

    >>> :kind! Eval (Compare '[1, 3] '[1, 2])
    Eval (Compare '[1, 3] '[1, 2]) :: Ordering
    = GT

#### Instances

Instances details

type Eval (Compare ('Left _a :: Either a b) ('Right _b :: Either a b) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Left _a :: Either a b) ('Right _b :: Either a b) :: Ordering -> Type) = 'LT
type Eval (Compare ('Right _a :: Either a b) ('Left _b :: Either a b) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Right _a :: Either a b) ('Left _b :: Either a b) :: Ordering -> Type) = 'GT
type Eval (Compare ('Left a2 :: Either a1 b1) ('Left b2 :: Either a1 b1) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Left a2 :: Either a1 b1) ('Left b2 :: Either a1 b1) :: Ordering -> Type) = Eval (Compare a2 b2)
type Eval (Compare ('Right a3 :: Either a2 a1) ('Right b :: Either a2 a1) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Right a3 :: Either a2 a1) ('Right b :: Either a2 a1) :: Ordering -> Type) = Eval (Compare a3 b)
type Eval (Compare 'EQ 'GT) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'EQ 'GT) = 'LT
type Eval (Compare 'EQ 'LT) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'EQ 'LT) = 'GT
type Eval (Compare 'GT 'EQ) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'GT 'EQ) = 'GT
type Eval (Compare 'GT 'LT) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'GT 'LT) = 'GT
type Eval (Compare 'LT 'EQ) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'LT 'EQ) = 'LT
type Eval (Compare 'LT 'GT) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'LT 'GT) = 'LT
type Eval (Compare a a :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a a :: Ordering -> Type) = 'EQ
type Eval (Compare ('Just _a) ('Nothing :: Maybe a) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Just _a) ('Nothing :: Maybe a) :: Ordering -> Type) = 'GT
type Eval (Compare ('Nothing :: Maybe a) ('Just _b) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Nothing :: Maybe a) ('Just _b) :: Ordering -> Type) = 'LT
type Eval (Compare ('Nothing :: Maybe a) ('Nothing :: Maybe a) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Nothing :: Maybe a) ('Nothing :: Maybe a) :: Ordering -> Type) = 'EQ
type Eval (Compare ('Just a2) ('Just b) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('Just a2) ('Just b) :: Ordering -> Type) = Eval (Compare a2 b)
type Eval (Compare a b :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = CmpNat a b
type Eval (Compare a b :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = 'EQ
type Eval (Compare '(a3, a4) '(b1, b2) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare '(a3, a4) '(b1, b2) :: Ordering -> Type) = Eval (Compare a3 b1) <> Eval (Compare a4 b2)
type Eval (Compare '(a4, a5, a6) '(b1, b2, b3) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare '(a4, a5, a6) '(b1, b2, b3) :: Ordering -> Type) = (Eval (Compare a4 b1) <> Eval (Compare a5 b2)) <> Eval (Compare a6 b3)
type Eval (Compare 'False 'True) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'False 'True) = 'GT
type Eval (Compare 'True 'False) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare 'True 'False) = 'GT
type Eval (Compare a a :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a a :: Ordering -> Type) = 'EQ
type Eval (Compare (_x ': _xs) ('[] :: [a]) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare (_x ': _xs) ('[] :: [a]) :: Ordering -> Type) = 'GT
type Eval (Compare (x ': xs) (y ': ys) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare (x ': xs) (y ': ys) :: Ordering -> Type) = Eval (Compare x y) <> Eval (Compare xs ys)
type Eval (Compare ('[] :: [k]) (_y ': _ys) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('[] :: [k]) (_y ': _ys) :: Ordering -> Type) = 'LT
type Eval (Compare ('[] :: [k]) ('[] :: [k]) :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare ('[] :: [k]) ('[] :: [k]) :: Ordering -> Type) = 'EQ
type Eval (Compare a b :: Ordering -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (Compare a b :: Ordering -> Type) = CmpSymbol a b

data (<=) :: a -> a -> Exp Bool Source #

"Smaller than or equal to". Type-level version of `(`<=`)`.

### Example

Expand

    >>> :kind! Eval ("b" <= "a")
    Eval ("b" <= "a") :: Bool
    = False

#### Instances

Instances details

type Eval (a2 <= b :: Bool -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (a2 <= b :: Bool -> Type)

data (>=) :: a -> a -> Exp Bool Source #

"Greater than or equal to". Type-level version of `(`>=`)`.

### Example

Expand

    >>> :kind! Eval ("b" >= "a")
    Eval ("b" >= "a") :: Bool
    = True

#### Instances

Instances details

type Eval (a2 >= b :: Bool -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (a2 >= b :: Bool -> Type)

data (<) :: a -> a -> Exp Bool Source #

"Smaller than". Type-level version of `(`<`)`.

### Example

Expand

    >>> :kind! Eval ("a" < "b")
    Eval ("a" < "b") :: Bool
    = True

#### Instances

Instances details

type Eval (a2 < b :: Bool -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (a2 < b :: Bool -> Type)

data (>) :: a -> a -> Exp Bool Source #

"Greater than". Type-level version of `(`>`)`.

### Example

Expand

    >>> :kind! Eval ("b" > "a")
    Eval ("b" > "a") :: Bool
    = True

#### Instances

Instances details

type Eval (a2 > b :: Bool -> Type) Source # |
Instance details Defined in Fcf.Class.Ord type Eval (a2 > b :: Bool -> Type)

# Equality

data TyEq :: a -> b -> Exp Bool Source #

Type equality.

### Details

Expand

The base library also defines a similar `(`==`)`; it differs from `TyEq` in the following ways:

- `TyEq` is heterogeneous: its arguments may have different kinds;
- `TyEq` is reflexive: `TyEq a a` always reduces to `True` even if `a` is a variable.

#### Instances

Instances details

type Eval (TyEq a b :: Bool -> Type) Source # |
Instance details Defined in Fcf.Utils type Eval (TyEq a b :: Bool -> Type)