Copyright | (c) L. S. Leary 2025 |
---|---|
Safe Haskell | None |
Language | GHC2021 |
Data.Hetero.Evidence.AtLeast
Contents
Synopsis
- data AtLeast (r :: RoleKind) (a :: k) (b :: k) where
- reflAL :: forall {k} (r :: RoleKind) (a :: k). KnownRole r => AtLeast r a a
- symAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k). AtLeast r a b -> AtLeast r b a
- 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
- hetTransAL :: 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
- maxAL :: 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
- weakenAL :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k). (KnownRole r, KnownRole s, r <= s) => AtLeast s a b -> AtLeast r a b
- weakenALToEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k). KnownRole r => AtLeast r a b -> Exactly r a b
- innerAL :: forall {k1} {k2} (f :: k1 -> k2) (r :: RoleKind) (a :: k1) (b :: k1). SuperPhantom f => AtLeast r (f a) (f b) -> AtLeast r a b
AtLeast
data AtLeast (r :: RoleKind) (a :: k) (b :: k) where Source #
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 |
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.
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.
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
are equivalent, then so are the arguments.SuperPhantom
f