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.
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?