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

Data.Hetero.Role

Contents

Roles
- Constraints

Description

Singleton Roles and corresponding constraints.

Synopsis

data RoleKind
- = Phantom
- | Representational
- | Nominal
data Role (r :: RoleKind) where
- Phantom :: Role 'Phantom
- Representational :: Role 'Representational
- Nominal :: Role 'Nominal
class KnownRole (r :: RoleKind) where
- knownRole :: Role r
expositRole :: forall (r :: RoleKind) s. Role r -> (KnownRole r => s) -> s
type IsPhantom (f :: k -> l) = forall (x :: k) (y :: k). Coercible (f x) (f y)
type IsRepresentational (f :: k -> l) = (SubNominal f, SuperPhantom f)
type IsNominal (f :: k -> l) = forall (x :: k) (y :: k). Coercible (f x) (f y) => x ~ y
type SubNominal (f :: k -> l) = forall (x :: k) (y :: k). Coercible x y => Coercible (f x) (f y)
type SuperPhantom (f :: k -> l) = forall (x :: k) (y :: k). Coercible (f x) (f y) => Coercible x y

Roles

data RoleKind Source #

The kind of roles.

Constructors

Phantom
Representational
Nominal

Instances

Instances details

BoundedAbove RoleKind Source #

Instance details

Defined in Data.Hetero.Role

Associated Types

type UpperBound RoleKind
Instance details Defined in Data.Hetero.Role type UpperBound RoleKind = 'Nominal

Methods

upperBound :: Sing RoleKind (UpperBound RoleKind) #

greatest :: forall (a :: RoleKind). Sing RoleKind a -> Proof (a <= UpperBound RoleKind) #

BoundedBelow RoleKind Source #

Instance details

Defined in Data.Hetero.Role

Associated Types

type LowerBound RoleKind
Instance details Defined in Data.Hetero.Role type LowerBound RoleKind = 'Phantom

Methods

lowerBound :: Sing RoleKind (LowerBound RoleKind) #

least :: forall (a :: RoleKind). Sing RoleKind a -> Proof (LowerBound RoleKind <= a) #

Equivalence RoleKind Source #

Instance details

Defined in Data.Hetero.Role

Methods

(=?) :: forall (a :: RoleKind) (b :: RoleKind). Sing RoleKind a -> Sing RoleKind b -> Either ((a :~: b) -> Void) (a :~: b) #

refl :: forall (a :: RoleKind). Sing RoleKind a -> Proof (a == a) #

sub :: forall (a :: RoleKind) (b :: RoleKind). a == b => Sing RoleKind a -> Sing RoleKind b -> a :~: b #

TotalOrder RoleKind Source #

Instance details

Defined in Data.Hetero.Role

Methods

(<|=|>) :: forall (a :: RoleKind) (b :: RoleKind). Sing RoleKind a -> Sing RoleKind b -> OrderingI a b #

antiSym :: forall (a :: RoleKind) (b :: RoleKind). Sing RoleKind a -> Sing RoleKind b -> Compare a b :~: Reflect (Compare b a) #

transLeq :: forall (a :: RoleKind) (b :: RoleKind) (c :: RoleKind). (a <= b, b <= c) => Sing RoleKind a -> Sing RoleKind b -> Sing RoleKind c -> Proof (a <= c) #

TestEquality Role Source #

Instance details

Defined in Data.Hetero.Role

Methods

testEquality :: forall (a :: RoleKind) (b :: RoleKind). Role a -> Role b -> Maybe (a :~: b) #

HetEq Role Source #

Instance details

Defined in Data.Hetero.Eq

Associated Types

type Strength Role
Instance details Defined in Data.Hetero.Eq type Strength Role = Strength (TestEq Role)

Methods

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

type LowerBound RoleKind Source #

Instance details

Defined in Data.Hetero.Role

type LowerBound RoleKind = 'Phantom

type Sing RoleKind Source #

Instance details

Defined in Data.Hetero.Role

type Sing RoleKind = Role

type UpperBound RoleKind Source #

Instance details

Defined in Data.Hetero.Role

type UpperBound RoleKind = 'Nominal

type Strength Role Source #

Instance details

Defined in Data.Hetero.Eq

type Strength Role = Strength (TestEq Role)

type Compare (a :: RoleKind) (b :: RoleKind) Source #

Instance details

Defined in Data.Hetero.Role

type Compare (a :: RoleKind) (b :: RoleKind)

data Role (r :: RoleKind) where Source #

Singleton roles.

Constructors

Phantom :: Role 'Phantom
Representational :: Role 'Representational
Nominal :: Role 'Nominal

Instances

Instances details

TestEquality Role Source #

Instance details

Defined in Data.Hetero.Role

Methods

testEquality :: forall (a :: RoleKind) (b :: RoleKind). Role a -> Role b -> Maybe (a :~: b) #

HetEq Role Source #

Instance details

Defined in Data.Hetero.Eq

Associated Types

type Strength Role
Instance details Defined in Data.Hetero.Eq type Strength Role = Strength (TestEq Role)

Methods

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

type Strength Role Source #

Instance details

Defined in Data.Hetero.Eq

type Strength Role = Strength (TestEq Role)

class KnownRole (r :: RoleKind) where Source #

Get the unique value corresponding to a RoleKind.

Methods

knownRole :: Role r Source #

Instances

Instances details

KnownRole 'Nominal Source #
Instance details Defined in Data.Hetero.Role Methods knownRole :: Role 'Nominal Source #
KnownRole 'Phantom Source #
Instance details Defined in Data.Hetero.Role Methods knownRole :: Role 'Phantom Source #
KnownRole 'Representational Source #
Instance details Defined in Data.Hetero.Role Methods knownRole :: Role 'Representational Source #

expositRole :: forall (r :: RoleKind) s. Role r -> (KnownRole r => s) -> s Source #

Make a Role known.

Constraints

type IsPhantom (f :: k -> l) = forall (x :: k) (y :: k). Coercible (f x) (f y) Source #

type IsRepresentational (f :: k -> l) = (SubNominal f, SuperPhantom f) Source #

type IsNominal (f :: k -> l) = forall (x :: k) (y :: k). Coercible (f x) (f y) => x ~ y Source #

type SubNominal (f :: k -> l) = forall (x :: k) (y :: k). Coercible x y => Coercible (f x) (f y) Source #

type SuperPhantom (f :: k -> l) = forall (x :: k) (y :: k). Coercible (f x) (f y) => Coercible x y Source #