Copyright	(c) L. S. Leary 2025
Safe Haskell	None
Language	GHC2021

Data.Hetero.Ord

Contents

HetOrdering
HetOrd

Description

Heterogeneous comparison with evidence capture.

Synopsis

data HetOrdering (r :: RoleKind) (a :: k) (b :: k)
- = HLT
- | HEQ (AtLeast r a b)
- | HGT
mapHO :: forall {k1} {k2} (r :: RoleKind) (a :: k1) (b :: k1) (s :: RoleKind) (c :: k2) (d :: k2). (AtLeast r a b -> AtLeast s c d) -> HetOrdering r a b -> HetOrdering s c d
bindHO :: forall {k1} {k2} (r :: RoleKind) (a :: k1) (b :: k1) (s :: RoleKind) (c :: k2) (d :: k2). HetOrdering r a b -> (AtLeast r a b -> HetOrdering s c d) -> HetOrdering s c d
class HetEq f => HetOrd (f :: k -> Type) where
- hcompare :: forall (a :: k) (b :: k). f a -> f b -> HetOrdering (Strength f) a b
type HetOrd' (f :: k -> Type) = (KnownRole (Strength f), HetOrd f)
defaultHEq :: forall {k} f (a :: k) (b :: k). HetOrd f => f a -> f b -> Maybe (AtLeast (Strength f) a b)
hcompareVia :: forall {k} f y (a :: k) (b :: k). (HetEq f, Ord y) => (forall (x :: k). f x -> y) -> f a -> f b -> HetOrdering (Strength f) a b

HetOrdering

data HetOrdering (r :: RoleKind) (a :: k) (b :: k) Source #

Ordering with captured evidence.

Constructors

HLT
HEQ (AtLeast r a b)
HGT

mapHO Source #

Arguments

:: forall {k1} {k2} (r :: RoleKind) (a :: k1) (b :: k1) (s :: RoleKind) (c :: k2) (d :: k2). (AtLeast r a b -> AtLeast s c d)
-> HetOrdering r a b
-> HetOrdering s c d

Map over the contained AtLeast r a b.

bindHO Source #

Arguments

:: forall {k1} {k2} (r :: RoleKind) (a :: k1) (b :: k1) (s :: RoleKind) (c :: k2) (d :: k2). HetOrdering r a b
-> (AtLeast r a b -> HetOrdering s c d)
-> HetOrdering s c d

Bind the contained AtLeast r a b.

HetOrd

class HetEq f => HetOrd (f :: k -> Type) where Source #

Heterogeneous comparison with evidence capture of type equivalence.

Methods

hcompare :: forall (a :: k) (b :: k). f a -> f b -> HetOrdering (Strength f) a b Source #

Compare an f a and an f b, opportunistically capturing the strongest type-equivalence evidence we can given the arguments.

Instances

Instances details

HetOrd SNat Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> HetOrdering (Strength SNat) a b Source #
HetOrd Role Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: RoleKind) (b :: RoleKind). Role a -> Role b -> HetOrdering (Strength Role) a b Source #
HetOrd SChar Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> HetOrdering (Strength SChar) a b Source #
HetOrd SSymbol Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> HetOrdering (Strength SSymbol) a b Source #
HetOrd (Proxy :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: k) (b :: k). Proxy a -> Proxy b -> HetOrdering (Strength (Proxy :: k -> Type)) a b Source #
HetOrd (TypeRep :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> HetOrdering (Strength (TypeRep :: k -> Type)) a b Source #
HetOrd (ID :: k -> Type) Source #
Instance details Defined in Data.Hetero.ID Methods hcompare :: forall (a :: k) (b :: k). ID a -> ID b -> HetOrdering (Strength (ID :: k -> Type)) a b Source #
HetOrd (VoidF :: k -> Type) Source #
Instance details Defined in Data.Hetero.Void Methods hcompare :: forall (a :: k) (b :: k). VoidF a -> VoidF b -> HetOrdering (Strength (VoidF :: k -> Type)) a b Source #
Ord a => HetOrd (Const a :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a0 :: k) (b :: k). Const a a0 -> Const a b -> HetOrdering (Strength (Const a :: k -> Type)) a0 b Source #
HetOrd (Coercion a :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a0 :: k) (b :: k). Coercion a a0 -> Coercion a b -> HetOrdering (Strength (Coercion a)) a0 b Source #
HetOrd ((:~:) a :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> HetOrdering (Strength ((:~:) a)) a0 b Source #
(HetOrd' f, HetOrd' g) => HetOrd (Product f g :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: k) (b :: k). Product f g a -> Product f g b -> HetOrdering (Strength (Product f g)) a b Source #
(HetOrd' f, HetOrd' g) => HetOrd (Sum f g :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: k) (b :: k). Sum f g a -> Sum f g b -> HetOrdering (Strength (Sum f g)) a b Source #
HetOrd ((:~~:) a :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> HetOrdering (Strength ((:~~:) a :: k -> Type)) a0 b Source #
HetOrd (AtLeast r a :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a0 :: k) (b :: k). AtLeast r a a0 -> AtLeast r a b -> HetOrdering (Strength (AtLeast r a)) a0 b Source #
HetOrd (Exactly r a :: k -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a0 :: k) (b :: k). Exactly r a a0 -> Exactly r a b -> HetOrdering (Strength (Exactly r a)) a0 b Source #
(HetOrd f, SuperPhantom g) => HetOrd (Compose f g :: k2 -> Type) Source #
Instance details Defined in Data.Hetero.Ord Methods hcompare :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> HetOrdering (Strength (Compose f g)) a b Source #

type HetOrd' (f :: k -> Type) = (KnownRole (Strength f), HetOrd f) Source #

defaultHEq :: forall {k} f (a :: k) (b :: k). HetOrd f => f a -> f b -> Maybe (AtLeast (Strength f) a b) Source #

A default implementation of heq in terms of hcompare.

hcompareVia Source #

Arguments

:: forall {k} f y (a :: k) (b :: k). (HetEq f, Ord y)
=> (forall (x :: k). f x -> y)
-> f a
-> f b
-> HetOrdering (Strength f) a b

An implementation of hcompare in terms of heq and a strictly increasing unifier.