heterogeneous-comparison
Copyright(c) L. S. Leary 2025
Safe HaskellNone
LanguageGHC2021

Data.Hetero.Evidence.Exactly

Contents

Description

Evidence Exactly corresponding to each Role.

Synopsis

Exactly

data Exactly (r :: RoleKind) (a :: k) (b :: k) where Source #

Evidence of equivalence, exactly corresponding to an associated role.

RoleEquivalenceEvidence
PhantomTrivial/Universal()
RepresentationalRepresentationalCoercible a b
NominalNominala ~ b

Constructors

PhantEx :: forall {k} (a :: k) (b :: k). Exactly 'Phantom a b 
ReprEx :: forall {k} (a :: k) (b :: k). Coercible a b => Exactly 'Representational a b 
NomEx :: forall {k} (a :: k). Exactly 'Nominal a a 

Instances

Instances details
KnownRole r => Category (Exactly r :: k -> k -> Type) Source # 
Instance details

Defined in Data.Hetero.Evidence.Exactly

Methods

id :: forall (a :: k). Exactly r a a #

(.) :: forall (b :: k) (c :: k) (a :: k). Exactly r b c -> Exactly r a b -> Exactly r a c #

HetEq (Exactly r a :: k -> Type) Source # 
Instance details

Defined in Data.Hetero.Eq

Associated Types

type Strength (Exactly r a :: k -> Type) 
Instance details

Defined in Data.Hetero.Eq

type Strength (Exactly r a :: k -> Type) = r

Methods

heq :: forall (a0 :: k) (b :: k). Exactly r a a0 -> Exactly r a b -> Maybe (AtLeast (Strength (Exactly 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 #

type Strength (Exactly r a :: k -> Type) Source # 
Instance details

Defined in Data.Hetero.Eq

type Strength (Exactly r a :: k -> Type) = r

roleEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k). Exactly r a b -> Role r Source #

The Role to which a piece of evidence Exactly corresponds.

reflEx :: forall {k} (r :: RoleKind) (a :: k). KnownRole r => Exactly r a a Source #

Reflexivity.

symEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k). Exactly r a b -> Exactly r b a Source #

Symmetry.

transEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k). Exactly r a b -> Exactly r b c -> Exactly r a c Source #

Role-homogeneous transitivity.

hetTransEx Source #

Arguments

:: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k) (c :: k). Exactly r a b 
-> Exactly s b c 
-> Exactly (Min r s) a c 

Exactly is a category graded by the Min monoid on RoleKind with identity:

NomEx :: Exactly Nominal a a

maxEx Source #

Arguments

:: forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind). Exactly r a b 
-> Exactly s a b 
-> Exactly (Max r s) a b 

Exactly _ a b is a monoid graded by the Max monoid on RoleKind with identity:

PhantEx :: Exactly Phantom a b

weakenEx :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k). (KnownRole r, r <= s) => Exactly s a b -> Exactly r a b Source #

Weaken evidence for one Role to evidence for a lesser Role.

applyEx Source #

Arguments

:: forall {k1} {k2} (g :: k1 -> k2) (r :: RoleKind) (f :: k1 -> k2) (a :: k1) (b :: k1). SubNominal g 
=> Exactly r f g 
-> Exactly r a b 
-> Exactly r (f a) (g b) 

If SubNominal functions and their arguments are equivalent, then so are their respective applications.

innerEx Source #

Arguments

:: forall {k1} {k2} (f :: k1 -> k2) (r :: RoleKind) (a :: k1) (b :: k1). SuperPhantom f 
=> Exactly r (f a) (f b) 
-> Exactly r a b 

If applications by SuperPhantom f are equivalent, then so are the arguments.