Choreography.Locations.Batteries

Additional functions/relations pertaining to locations and type-level lists of locations.

Misc

class ExplicitMember (x :: k) (xs :: [k]) where

Quickly build membership proofs, when the membership can be directly observed by GHC.

Methods

explicitMember :: Member x xs

Instances

ExplicitMember (x :: a) (x ': xs :: [a])

Defined in Choreography.Locations.Batteries

Methods

explicitMember :: Member x (x ': xs)

ExplicitMember x xs => ExplicitMember (x :: a) (y ': xs :: [a])

Defined in Choreography.Locations.Batteries

Methods

explicitMember :: Member x (y ': xs)

class ExplicitSubset xs ys where

Quickly build subset proofs, when the subset relation can be directly observed by GHC.

Methods

explicitSubset :: Subset xs ys

Instances

ExplicitSubset ('[] :: [k]) (ys :: [k])

Defined in Choreography.Locations.Batteries

Methods

explicitSubset :: Subset '[] ys

(ExplicitSubset xs ys, ExplicitMember x ys) => ExplicitSubset (x ': xs :: [k]) (ys :: [k])

Defined in Choreography.Locations.Batteries

Methods

explicitSubset :: Subset (x ': xs) ys

allOf :: forall ps. Subset ps ps

Alias refl. When used as an identifier, this is more descriptive.

singleton :: forall p. Member p (p ': '[])

Any element p is a member of the list '[p].

Easy indexing with Member objects.

listedFirst :: forall p1 ps. Member p1 (p1 ': ps)

A Member value for the first item in a list. Note that type-applicaiton is different than with First, to which this is otherwise redundant.

listedSecond :: forall p2 p1 ps. Member p2 (p1 ': (p2 ': ps))

A Member value for the second item in a list.

listedThird :: forall p3 p2 p1 ps. Member p3 (p1 ': (p2 ': (p3 ': ps)))

A Member value for the third item in a list.

listedForth :: forall p4 p3 p2 p1 ps. Member p4 (p1 ': (p2 ': (p3 ': (p4 ': ps))))

A Member value for the forth item in a list.

listedFifth :: forall p5 p4 p3 p2 p1 ps. Member p5 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': ps)))))

A Member value for the fifth item in a list.

listedSixth :: forall p6 p5 p4 p3 p2 p1 ps. Member p6 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': (p6 ': ps))))))

A Member value for the sixth item in a list.

Context manipulation

quorum1 :: forall ps p a. KnownSymbols ps => Member p ps -> (forall q qs. (KnownSymbol q, KnownSymbols qs, ps ~ (q ': qs)) => a) -> a

Use any membership proof to to safely call code that only works on a non-empy list.

Template Haskell

mkLoc :: String -> Q [Dec]

Declare a proof-value with the given string as the variable name, proving that that string is a member of any list in which it explicitly apprears.