| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Choreography.Locations.Batteries
Description
Additional functions/relations pertaining to locations and type-level lists of locations.
Synopsis
- class ExplicitMember (x :: k) (xs :: [k]) where
- explicitMember :: Member x xs
- class ExplicitSubset (xs :: [k]) (ys :: [k]) where
- explicitSubset :: Subset xs ys
- allOf :: forall {k} (ps :: [k]). Subset ps ps
- singleton :: forall {a} (p :: a). Member p '[p]
- listedFirst :: forall {a} (p1 :: a) (ps :: [a]). Member p1 (p1 ': ps)
- listedSecond :: forall {a} (p2 :: a) (p1 :: a) (ps :: [a]). Member p2 (p1 ': (p2 ': ps))
- listedThird :: forall {a} (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p3 (p1 ': (p2 ': (p3 ': ps)))
- listedForth :: forall {a} (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p4 (p1 ': (p2 ': (p3 ': (p4 ': ps))))
- listedFifth :: forall {a} (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p5 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': ps)))))
- listedSixth :: forall {a} (p6 :: a) (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p6 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': (p6 ': ps))))))
- quorum1 :: forall (ps :: [Symbol]) (p :: Symbol) a. KnownSymbols ps => Member p ps -> (forall (q :: Symbol) (qs :: [Symbol]). (KnownSymbol q, KnownSymbols qs, ps ~ (q ': qs)) => a) -> a
- mkLoc :: String -> Q [Dec]
Misc
class ExplicitMember (x :: k) (xs :: [k]) where Source #
Quickly build membership proofs, when the membership can be directly observed by GHC.
Methods
explicitMember :: Member x xs Source #
Instances
| ExplicitMember (x :: a) (x ': xs :: [a]) Source # | |
Defined in Choreography.Locations.Batteries Methods explicitMember :: Member x (x ': xs) Source # | |
| ExplicitMember x xs => ExplicitMember (x :: a) (y ': xs :: [a]) Source # | |
Defined in Choreography.Locations.Batteries Methods explicitMember :: Member x (y ': xs) Source # | |
class ExplicitSubset (xs :: [k]) (ys :: [k]) where Source #
Quickly build subset proofs, when the subset relation can be directly observed by GHC.
Methods
explicitSubset :: Subset xs ys Source #
Instances
| ExplicitSubset ('[] :: [k]) (ys :: [k]) Source # | |
Defined in Choreography.Locations.Batteries Methods explicitSubset :: Subset ('[] :: [k]) ys Source # | |
| (ExplicitSubset xs ys, ExplicitMember x ys) => ExplicitSubset (x ': xs :: [k]) (ys :: [k]) Source # | |
Defined in Choreography.Locations.Batteries Methods explicitSubset :: Subset (x ': xs) ys Source # | |
allOf :: forall {k} (ps :: [k]). Subset ps ps Source #
Alias refl. When used as an identifier, this is more descriptive.
Easy indexing with Member objects.
listedFirst :: forall {a} (p1 :: a) (ps :: [a]). Member p1 (p1 ': ps) Source #
listedSecond :: forall {a} (p2 :: a) (p1 :: a) (ps :: [a]). Member p2 (p1 ': (p2 ': ps)) Source #
A Member value for the second item in a list.
listedThird :: forall {a} (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p3 (p1 ': (p2 ': (p3 ': ps))) Source #
A Member value for the third item in a list.
listedForth :: forall {a} (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p4 (p1 ': (p2 ': (p3 ': (p4 ': ps)))) Source #
A Member value for the forth item in a list.
listedFifth :: forall {a} (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p5 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': ps))))) Source #
A Member value for the fifth item in a list.
listedSixth :: forall {a} (p6 :: a) (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]). Member p6 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': (p6 ': ps)))))) Source #
A Member value for the sixth item in a list.
Context manipulation
quorum1 :: forall (ps :: [Symbol]) (p :: Symbol) a. KnownSymbols ps => Member p ps -> (forall (q :: Symbol) (qs :: [Symbol]). (KnownSymbol q, KnownSymbols qs, ps ~ (q ': qs)) => a) -> a Source #
Use any membership proof to to safely call code that only works on a non-empy list.