Computing on party sets in Wysteria.

committee.md

Election in Wysteria

Attempt 1

The most natural way to try express the elect function in Wysteria is using its support for first-class party sets.

let elect (parties : ps{true}) (n : nat) : ps{subeq parties} = ??

This version of the function takes a party set, parties, about which we know nothing (ps{true}) and gives back a party set which is a subset of parties (ps{subeq parties}). Unfortunately, there is no way to write this function in Wysteria because there is no elimination form for party sets.

Fortunately, Aseem's code hints at an encoding which gets us a little further.

Attempt 2

In this iteration, we will encode a party set as an array of singleton party sets.

let elect (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) (n : nat) : array ps{singl and subeq parties} =
  let ret = array [ n ] of (select parties_enc[0]) in
  let rec elect_r i =
    if i < n then
      let _ = update ret[i] <- (select parties_enc[i]) in
      elect_r (i + 1)
    else
      ()
  in
  let _ = elect_r 0 in
  ret

This function works and is well-typed. Let's try to use our elect function to elect a committee and execute a function among the committee.

let foo (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) : ... = ...

let parties       = { !A, !B, !C } in
let parties_enc   = ... in
let committee_enc = elect parties parties_enc 2 in
let ret =par(??)=
  foo ?? committee_enc
in ret

Unfortunately, we cannot pass our encoding to par because it expects a party set. So, now we must figure out how to "extract" a party set from an encoding. Fortunately, this is also possible!

let decode (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) : ps{subeq parties} =
  let n = length parties_enc in
  let rec loop i acc =
    if i < n then
      let p = select parties_enc[i] in
      loop (i + 1) (acc ∪ p)
    else
      acc
  in loop 0 { }

Caveat: Wysteria does not support computing the length of an array as we have on line 2, but this feature could be added easily.

Now that we have our decode function, let's try to continue with our example.

let foo (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) : ... = ...

let parties       = { !A, !B, !C } in
let parties_enc   = ... in
let committee_enc = elect parties parties_enc 2 in
let committee     = decode parties committee_enc in
let ret =par(committee)=
  foo committee committee_enc
in ret

This almost works, but unfortunately the type checker will reject this program on the call to foo. To see why, let's add some type annotations.

let foo (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) : ... = ...

let parties       : ps{true} = { !A, !B, !C } in
let parties_enc   : array ps{singl and subeq parties} = ... in
let committee_enc : array ps{singl and subeq parties} = elect parties parties_enc 2 in
let committee     : ps{subeq parties} = decode parties committee_enc in
let ret =par(committee)=
  foo committee committee_enc
in ret

The call to foo requires that committee_enc have type ps{singl and subeq committee}. There are some ways that, in theory, we could try to continue to make progress. For example, with a dependent pair type, we could refine the type of decode:

let decode (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) : Σ ret : ps{subeq parties} . array ps{singl and subeq ret} = ...

Then we could accomplish what we want.

let foo (parties : ps{true}) (parties_enc : array ps{singl and subeq parties}) : ... = ...

let parties       : ps{true} = { !A, !B, !C } in
let parties_enc   : array ps{singl and subeq parties} = ... in
let committee_enc : array ps{singl and subeq parties} = elect parties parties_enc 2 in
let (committee : ps{subeq parties}, committee_enc : array ps{singl and subeq committee}) = decode parties committee_enc in
let ret =par(committee)=
  foo committee committee_enc
in ret

There may also be ways to avoid using dependent pairs by improving the expresiveness of the refinement types. In particular, I imagine you'd need to be able to refine arrays and add constraints of the sort "the union of all the elements is p". At that point, though, you've fully reflected the party set into the array. In other words, you singleton types for party sets.

Thoughts?