Copyright | (c) L. S. Leary 2025 |
---|---|
Safe Haskell | None |
Language | GHC2021 |
Data.Hetero.Evidence.Exactly
Contents
Synopsis
- data Exactly (r :: RoleKind) (a :: k) (b :: k) where
- roleEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k). Exactly r a b -> Role r
- reflEx :: forall {k} (r :: RoleKind) (a :: k). KnownRole r => Exactly r a a
- symEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k). Exactly r a b -> Exactly r b a
- transEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k). Exactly r a b -> Exactly r b c -> Exactly r a c
- hetTransEx :: 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
- maxEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind). Exactly r a b -> Exactly s a b -> Exactly (Max r s) 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
- applyEx :: 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)
- innerEx :: forall {k1} {k2} (f :: k1 -> k2) (r :: RoleKind) (a :: k1) (b :: k1). SuperPhantom f => Exactly r (f a) (f b) -> Exactly r a b
Exactly
data Exactly (r :: RoleKind) (a :: k) (b :: k) where Source #
Evidence of equivalence, exactly corresponding to an associated role.
Role | Equivalence | Evidence |
---|---|---|
Phantom | Trivial/Universal | () |
Representational | Representational |
|
Nominal | Nominal | a ~ 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 |
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.
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
.
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.
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
are equivalent, then so are the arguments.SuperPhantom
f