Value-level proofs of type-level membership and subset relations in Haskell

Question

As part of a larger project, we're using type-level strings to identify "parties" (synonymously, "locations"). Critical to the system is the ability to express and enforce constraints like "In order to call f @"Alice" x, "Alice" must be a member of such-n-such type level list." Note that "Alice" in this context is a type level string, AKA a Symbol or a LocTy. Significantly, expressions can be polymorphic with respect to the type level list that they need to be enforcing membership in!

Our basic strategy is to use proof objects à la GDP. Things worked out a little nicer rolling our own system than using the gdp library itself, and that's what this post is about.

The advantage of such a system (over more obvious options like type constraints) is that it allows us to manipulate knowledge of membership and subset relations actively and intuitively. For example a property like

(p ∈ ps1 ∧ ps1 ⊆ ps2) → p ∈ ps2

is represented in the below code by the function (record field) inSuper. Surprisingly, refl turns out to be especially important and especially hard to write using purely type-level programming, but with proof-objects it's easy.

Here's the core module, which includes all the important building blocks:

import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
-- * Type aliases
-- | Term-level locations.
type LocTm = String
-- | Type-level locations.
type LocTy = Symbol
-- * Membership and Subset proofs
-- | 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.
data Member (x :: k) (xs :: [k]) where
 First :: forall xs x xs'. (xs ~ (x ': xs')) => Member x (x ': xs')
 Later :: Member x xs -> Member x (y ': xs)
-- | 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.)
newtype Subset xs ys = Subset
 { -- | Convert a proof of membership in the sublist to a proof of membership in the superlist.
 -- Frequently used to show that a location is part of a larger set of locations.
 inSuper :: forall x. Member x xs -> Member x ys
 }
-- | The subset relation is reflexive.
refl :: Subset xs xs
refl = Subset id
-- | The sublist relation is transitive.
transitive :: Subset xs ys -> Subset ys zs -> Subset xs zs
transitive sxy syz = Subset $ inSuper syz . inSuper sxy
-- | The `[]` case of subset proofs.
-- Typlically used to build subset proofs using membership proofs using `@@`.
nobody :: Subset '[] ys
nobody = Subset \case {}
-- | Any lists is a subset of the list made by consing itself with any other item.
consSet :: forall xs x xs'. (xs ~ (x ': xs')) => Subset xs' (x ': xs')
consSet = Subset Later
-- | Cons an element to the superset in a t`Subset` value.
consSuper :: forall xs ys y. Subset xs ys -> Subset xs (y ': ys)
consSuper sxy = transitive sxy consSet
-- | Cons an element to the subset in a t`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
(@@) :: Member x ys -> Subset xs ys -> Subset (x ': xs) ys
infixr 5 @@
mxy @@ sxy = Subset \case
 First -> mxy
 Later mxxs -> inSuper sxy mxxs
-- * Accessing parties' names
-- | Convert a proof-level location to a term-level location.
toLocTm ::
 forall (l :: LocTy) (ps :: [LocTy]).
 (KnownSymbol l) =>
 Member l ps ->
 LocTm
toLocTm _ = symbolVal (Proxy @l)
-- | Get the term-level list of names-as-strings for a proof-level list of parties.
toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]). (KnownSymbols ls) => Subset ls ps -> [LocTm]
toLocs _ = case tySpine @ls of -- this could be golfed by Quire, if that were defined here.
 TyNil -> []
 TyCons -> toLocTm (First @ls) : toLocs (consSet @ls)
-- * Handling type-level lists literals
-- $Handling
--
-- `KnownSymbols` constraints will often need to be declared in user code,
-- but using `tySpine` should only be necessary
-- when the behavior of a program depends on the structure of the type-level lists.
-- Most of the time existing functions will do this for you.
-- | 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.
data TySpine ps where
 -- | Denotes that the list has a head and tail, and exposes `KnownSymbol` and `KnownSymbols` constraints respectively.
 TyCons :: (KnownSymbol h, KnownSymbols ts) => TySpine (h ': ts)
 -- | Denotes that the list is empty.
 TyNil :: TySpine '[]
-- | The type-level-list version of `GHC.TypeList.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@.
class KnownSymbols ls where
 -- | 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.
 tySpine :: TySpine ls
instance KnownSymbols '[] where
 tySpine = TyNil
instance (KnownSymbols ls, KnownSymbol l) => KnownSymbols (l ': ls) where
 tySpine = TyCons

And here's a "batteries" module, which includes some derived functions that turned out to be useful. Included in this is, in effect, exactly the constraints system I said wasn't good enough, because in some situations it is good enough, and when it does work it's more concise.

import GHC.TypeLits (KnownSymbol)
import Language.Haskell.TH
-- * Misc
-- | Quickly build membership proofs, when the membership can be directly observed by GHC.
class ExplicitMember (x :: k) (xs :: [k]) where
 explicitMember :: Member x xs
instance {-# OVERLAPPABLE #-} (ExplicitMember x xs) => ExplicitMember x (y ': xs) where
 explicitMember = inSuper consSet explicitMember
instance {-# OVERLAPS #-} ExplicitMember x (x ': xs) where
 explicitMember = First
-- | Quickly build subset proofs, when the subset relation can be directly observed by GHC.
class ExplicitSubset xs ys where
 explicitSubset :: Subset xs ys
instance {-# OVERLAPPABLE #-} (ExplicitSubset xs ys, ExplicitMember x ys) => ExplicitSubset (x ': xs) ys where
 explicitSubset = explicitMember @@ explicitSubset
instance {-# OVERLAPS #-} ExplicitSubset '[] ys where
 explicitSubset = nobody
-- | Alias `refl`. When used as an identifier, this is more descriptive.
allOf :: forall ps. Subset ps ps
allOf = refl
-- | Any element @p@ is a member of the list @'[p]@.
singleton :: forall p. Member p (p ': '[])
singleton = First
-- * Easy indexing with `Member` objects.
-- | 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.
listedFirst :: forall p1 ps. Member p1 (p1 ': ps) -- Can we replace all of these with something using off-the-shelf type-level Nats?
listedFirst = First
-- | A `Member` value for the second item in a list.
listedSecond :: forall p2 p1 ps. Member p2 (p1 ': p2 ': ps)
listedSecond = inSuper (consSuper refl) listedFirst
-- | A `Member` value for the third item in a list.
listedThird :: forall p3 p2 p1 ps. Member p3 (p1 ': p2 ': p3 ': ps)
listedThird = inSuper (consSuper refl) listedSecond
-- | A `Member` value for the forth item in a list.
listedForth :: forall p4 p3 p2 p1 ps. Member p4 (p1 ': p2 ': p3 ': p4 ': ps)
listedForth = inSuper (consSuper refl) listedThird
-- | A `Member` value for the fifth item in a list.
listedFifth :: forall p5 p4 p3 p2 p1 ps. Member p5 (p1 ': p2 ': p3 ': p4 ': p5 ': ps)
listedFifth = inSuper (consSuper refl) listedForth
-- | A `Member` value for the sixth item in a list.
listedSixth :: forall p6 p5 p4 p3 p2 p1 ps. Member p6 (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': ps)
listedSixth = inSuper (consSuper refl) listedFifth
-- * Context manipulation
-- | Use any membership proof to to safely call code that only works on a non-empy list.
quorum1 ::
 forall ps p a.
 (KnownSymbols ps) =>
 Member p ps ->
 (forall q qs. (KnownSymbol q, KnownSymbols qs, ps ~ q ': qs) => a) ->
 a
quorum1 p a = case (p, tySpine @ps) of
 (First, TyCons) -> a
 (Later _, TyCons) -> a
-- * Template Haskell
-- | 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.
mkLoc :: String -> Q [Dec]
mkLoc loc = do
 let locName = mkName loc
 let tvar = mkName "xs"
 let m = mkName "Member"
 let eM = mkName "ExplicitMember"
 let em = mkName "explicitMember"
 pure
 [ SigD
 locName
 ( ForallT
 [PlainTV tvar SpecifiedSpec]
 [AppT (AppT (ConT eM) (LitT (StrTyLit loc))) (VarT tvar)]
 (AppT (AppT (ConT m) (LitT (StrTyLit loc))) (VarT tvar))
 ),
 ValD (VarP locName) (NormalB (VarE em)) []
 ]

And here's a hopefully-digestible example of how it gets used. (Subsets gets used as both proofs and as identifiers, just like Members are used here.)

-- | Communicate a value to all present parties.
broadcast' ::
 (Show a, Read a, KnownSymbol l) =>
 -- | Proof the sender is present
 Member l ps ->
 -- | Proof the sender knows the value, the value.
 (Member l ls, Located ls a) ->
 Choreo ps m a
_locally ::
 (KnownSymbol l) =>
 Member l ps ->
 m a ->
 Choreo ps m (Located '[l] a)
example :: forall peers. (KnownSymbols peers) => Choreo ("Alice" ': peers) IO String
example = do
 let peers = consSuper (refl @peers)
 alice = listedFirst @"Alice"
 everyone = refl @("Alice" : peers)
 value <- _locally alice (getLine)
 broadcast' alice (singleton, value)

I'm happy to answer questions about all of this. Miscellaneous suggestions are always welcome! My particular questions for today are

• Have I re-invented anyone's wheel? If there's an off-the shelf system or a documented technique for doing this kind of thing then I really want to know about it!
• How would you go about adding support for more set operations? For example, we might like to write intersection :: Subset as ps -> Subset bs ps -> Subset (as ∩ bs) ps?
• In practice, we find that it's necessary to propagate KnownSymbol and KnownSymbols constraints everywhere. This is manageable, but not great. In particular, although we rarely need to convert between type-level Symbols and term-level Strings, it would be nice to have the ability to turn runtime strings into type-level party identifiers. I have some tentative ideas for compromises, but I'm hoping other people will have better ideas!

• ShapeOfMatter: Here's a link to the broader context, with the polite request that anyone involved in any formal peer-review processes skip over it :)
• J_H: typo nit: listedFourth. There's still time to fix it. Go forth and prosper!