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

Data.Hetero.Evidence.AtLeast

Contents

Description

Evidence AtLeast as strong as that Exactly corresponding to a given Role.

Synopsis

AtLeast

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

Evidence AtLeast as strong as that Exactly corresponding to a given Role.

Bundled Patterns

pattern AtLeast :: forall {k} r a b (s :: RoleKind). () => r <= s => Exactly s a b -> AtLeast r a b 
pattern PhantAL :: () => r <= 'Phantom => AtLeast r a b 
pattern ReprAL :: () => (r <= 'Representational, Coercible a b) => AtLeast r a b 
pattern NomAL :: () => (r <= 'Nominal, a ~ b) => AtLeast r a b 

Instances

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

Defined in Data.Hetero.Evidence.AtLeast.Internal

Methods

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

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

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

Defined in Data.Hetero.Eq

Associated Types

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

Defined in Data.Hetero.Eq

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

Methods

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

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

Defined in Data.Hetero.Eq

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

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

Reflexivity.

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

Symmetry.

transAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k). KnownRole r => AtLeast r a b -> AtLeast r b c -> AtLeast r a c Source #

Role-homogeneous transitivity.

hetTransAL Source #

Arguments

:: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k) (c :: k). (KnownRole r, KnownRole s) 
=> AtLeast r a b 
-> AtLeast s b c 
-> AtLeast (Min r s) a c 

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

NomAL :: AtLeast Nominal a a

maxAL Source #

Arguments

:: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k). (KnownRole r, KnownRole s) 
=> AtLeast r a b 
-> AtLeast s a b 
-> AtLeast (Max r s) a b 

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

PhantAL :: AtLeast Phantom a b

weakenAL Source #

Arguments

:: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k). (KnownRole r, KnownRole s, r <= s) 
=> AtLeast s a b 
-> AtLeast r a b 

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

weakenALToEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k). KnownRole r => AtLeast r a b -> Exactly r a b Source #

Weaken inexact evidence to exact evidence of the same role.

innerAL Source #

Arguments

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

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