| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Choreography.Locations
Description
This module defines locations (AKA parties) and functions/relations pertaining to type-level lists of locations.
Synopsis
- type LocTm = String
- type LocTy = Symbol
- data Member (x :: k) (xs :: [k]) where
- newtype Subset xs ys = Subset {}
- refl :: Subset xs xs
- transitive :: Subset xs ys -> Subset ys zs -> Subset xs zs
- nobody :: Subset '[] ys
- consSet :: forall xs x xs'. xs ~ (x ': xs') => Subset xs' (x ': xs')
- consSuper :: forall xs ys y. Subset xs ys -> Subset xs (y ': ys)
- (@@) :: Member x ys -> Subset xs ys -> Subset (x ': xs) ys
- toLocTm :: forall (l :: LocTy) (ps :: [LocTy]). KnownSymbol l => Member l ps -> LocTm
- toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]). KnownSymbols ls => Subset ls ps -> [LocTm]
- data TySpine ps where
- TyCons :: (KnownSymbol h, KnownSymbols ts) => TySpine (h ': ts)
- TyNil :: TySpine '[]
- class KnownSymbols ls where
Type aliases
Membership and Subset proofs
data Member (x :: k) (xs :: [k]) where Source #
A term-level proof that a LocTy is a member of a [LocTy].
These are frequently used both for proofs per se and to identify individuals in lists of locations.
For example: player :: Member players census is a proof that the type-level Symbol, player, is in census,
and it can also be used as a term-level identifier for the type-level player,
similar to how a proxy might be used.
Pattern matching on these values is like pattern matching on a successor-based Nat;
in this sense a Member x xs is an index into xs at which x can be found.
Constructors
| First :: forall xs x xs'. xs ~ (x ': xs') => Member x (x ': xs') | |
| Later :: Member x xs -> Member x (y ': xs) |
Instances
| (KnownSymbol l, ExplicitMember l ls) => CanSend (Member l ps, Located ls a) l a ls ps Source # | |
Defined in Choreography.Choreography | |
| KnownSymbol l => CanSend (Member l ps, (Member l ls, Located ls a)) l a ls ps Source # | |
Defined in Choreography.Choreography | |
| KnownSymbol l => CanSend (Member l ls, Subset ls ps, Located ls a) l a ls ps Source # | |
Defined in Choreography.Choreography | |
A term level proof that one type-level list represents a subset of another, embodied by a total function from proof-of-membership in the sublist to proof-of-membership in the superlist. (If you make one with a partial funciton, all bets are off.)
Constructors
| Subset | |
Instances
| KnownSymbol l => CanSend (Member l ls, Subset ls ps, Located ls a) l a ls ps Source # | |
Defined in Choreography.Choreography | |
transitive :: Subset xs ys -> Subset ys zs -> Subset xs zs Source #
The sublist relation is transitive.
nobody :: Subset '[] ys Source #
The `[]` case of subset proofs.
Typlically used to build subset proofs using membership proofs using @@.
consSet :: forall xs x xs'. xs ~ (x ': xs') => Subset xs' (x ': xs') Source #
Any lists is a subset of the list made by consing itself with any other item.
consSuper :: forall xs ys y. Subset xs ys -> Subset xs (y ': ys) Source #
Cons an element to the superset in a Subset value.
(@@) :: Member x ys -> Subset xs ys -> Subset (x ': xs) ys infixr 5 Source #
Cons an element to the subset in a Subset value;
requires proof that the new head element is already a member of the superset.
Used like ":" for subset proofs.
Suppose you have (alice :: Member Alice census)
and we want a subset proof instead of membership; we can write:
>>>proof :: Subset '["Alice"] census = alice @@ nobody
Accessing parties' names
toLocTm :: forall (l :: LocTy) (ps :: [LocTy]). KnownSymbol l => Member l ps -> LocTm Source #
Convert a proof-level location to a term-level location.
toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]). KnownSymbols ls => Subset ls ps -> [LocTm] Source #
Get the term-level list of names-as-strings for a proof-level list of parties.
Handling type-level lists literals
KnownSymbols constraints will often need to be declared in user code,
but using tySpine should only be necessary
when the behavior of the choreography depends on the structure of the type-level lists.
Most of the time the functions in Choreography.Polymorphism should do this for you.
data TySpine ps where Source #
Term-level markers of the spine/structure of a type-level list.
Pattern matching on them recovers both the spine of the list and, if applicable,
KnownSymbol[s] instances for the head and tail.
Constructors
| TyCons :: (KnownSymbol h, KnownSymbols ts) => TySpine (h ': ts) | Denotes that the list has a head and tail, and exposes |
| TyNil :: TySpine '[] | Denotes that the list is empty. |
class KnownSymbols ls where Source #
The type-level-list version of KnownSymbol.
Denotes that both the spine of the list and each of its elements is known at compile-time.
This knowlege is typically recovered by recursively pattern-matching on tySpine @ls.
Methods
tySpine :: TySpine ls Source #
Pattern matching on tySpine @ls will normally have two cases, for when ls is empty or not.
Contextual knowledge may let one or the other case be skipped.
Within those cases, the knowledge afforded by tySpine's constructors can be used.
Instances
| KnownSymbols ('[] :: [Symbol]) Source # | |
Defined in Choreography.Locations | |
| (KnownSymbols ls, KnownSymbol l) => KnownSymbols (l ': ls) Source # | |
Defined in Choreography.Locations | |