Macro mononym::exists [−][src]
macro_rules! exists {
($($exists : ident($name : ident : $type : ty) => $proof : ident
$(< $($proof_param : ident), + $(,) ? >) ?
($($suchthat : ident $(: $suchtype : ty) ?), * $(,) ?) ;) *) => { ... };
}
Expand description
Macro to define new named value coupled with proofs in the form of dependent pairs.
Suppose we have a named u64
integer and we want to
add 1 to the value using
checked addition
and return a new named u64
. Along the way,
we also want to construct a proof that shows that the new
u64
value is a successor of the original value.
We can define our successor proof similar to the other
proofs that are defined by proof!
, but when
we try to define our add_one
function, we would
hit a roadblock like follows:
mod successor {
use mononym::*;
proof! {
IsSuccessor(succ: u64, pred: u64);
}
pub fn add_one<NumVal: HasType<u64>>(
seed: Seed<impl Name>,
num: &Named<NumVal, u64>,
) -> Option<(Named<impl Name, u64>, IsSuccessor<??, NumVal>)>
{
todo!()
}
}
The issue with the return type of our add_one
function above is that
the type IsSuccessor<??, NumVal>
depends on the fresh name type
impl Name
in Named<impl Name, 64>
to fill in the hole of ??
.
This construct is known as a
dependent pair
in languages with dependent types such as Idris.
Although Rust do not have built in support for constructing dependent
pairs, we can still emulate that by wrapping the two return types
inside a new struct that we will call ExistSuccessor
:
mod successor {
use mononym::*;
use core::marker::PhantomData;
proof! {
IsSuccessor(succ: u64, pred: u64);
}
pub struct ExistSuccessor<
SuccVal: HasType<u64>,
PredVal: HasType<u64>,
> {
successor: Named<SuccVal, u64>,
is_successor: IsSuccessor<SuccVal, PredVal>,
}
fn new_exist_successor<
PredVal: HasType<u64>,
>
( seed: Seed<impl Name>,
succ: u64,
) -> ExistSuccessor<impl HasType<u64>, PredVal>
{
ExistSuccessor {
successor: seed.new_named(succ),
is_successor: IsSuccessor::new(),
}
}
pub fn add_one<NumVal: HasType<u64>>(
seed: Seed<impl Name>,
num: &Named<NumVal, u64>,
) -> Option<ExistSuccessor<impl HasType<u64>, NumVal>>
{
num.value()
.checked_add(1)
.map(|succ| new_exist_successor(seed, succ))
}
}
The ExistSuccessor
struct allows the same type parameter SuccVal
to be used in both Named
and IsSuccessor
. Using that, we can
redefine our add_one
function to return the type
ExistSuccessor<impl HasType<u64>, NumVal>
, which the fresh
name type impl HasType<u64>
can be used in both places.
Although the above solution works, there are quite a lot of
boilerplate required to define just one dependent pair type.
Therefore the exists!
macro is provided so that the same
definition above can be simplified into a single line definition
as shown below:
mod successor {
use mononym::*;
use core::marker::PhantomData;
exists! {
ExistSuccessor(succ: u64) => IsSuccessor(pred: u64);
}
pub fn add_one<NumVal: HasType<u64>>(
seed: Seed<impl Name>,
num: &Named<NumVal, u64>,
) -> Option<ExistSuccessor<impl HasType<u64>, NumVal>>
{
num.value()
.checked_add(1)
.map(|succ| new_exist_successor(seed, succ))
}
}
Note that the new version of the successor
module is the same as
the original version. The exists!
takes care of generating
the various struct definitions, as well as calling proof!
to generate the IsSuccessor
proof type.
One limitation of the exists!
macro is that the existential name
is always in the first position of the following proof type.
That is, the definition
exists! { ExistSuccessor(succ: u64) => IsSuccessor(pred: u64); }
leads to the call to
proof! { IsSuccessor(succ: u64, pred: u64); }
Therefore we cannot switch the position of the variables in the proof type, such as having
proof! { IsSuccessor(pred: u64, succ: u64); }