Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extendability problem #1

Open
constituent opened this issue Nov 25, 2021 · 0 comments
Open

Extendability problem #1

constituent opened this issue Nov 25, 2021 · 0 comments

Comments

@constituent
Copy link

Thanks for this wonderful library! I have played with it a bit, trying to apply to some simple but more realistic problems. What I found most frustrating is that I cannot figure out how to derive new proof with existing ones.

Take the less_than_eq proof as an example:

pub mod less_than_eq
{
  use mononym::*;

  proof! {
    LessThanEq(x: u32, y: u32);
  }

  pub fn check_less_than_eq<XVal: HasType<u32>, YVal: HasType<u32>>(
    x: &Named<XVal, u32>,
    y: &Named<YVal, u32>,
  ) -> Option<LessThanEq<XVal, YVal>>
  {
    if x.value() <= y.value() {
      Some(LessThanEq::new())
    } else {
      None
    }
  }
}

And I want to add a simple function:

pub fn at_most(x: u32, y: u32) -> u32 {
    if x <= y {
        x
    } else {
        y
    }
}

Ideally, I could write this function (with a LessThanEq<ZVal, YVal> proof) outside the less_than_eq module. However, what I finally struggled to achieve was something like this, inside less_than_eq module:

pub struct ExistLessThanEq<
    ZVal: HasType<u32>,
    YVal: HasType<u32>,
> {
    pub z: Named<ZVal, u32>,
    pub y: Named<YVal, u32>,
    pub less_than_eq: LessThanEq<ZVal, YVal>,
}

pub fn at_most(x: u32, y: u32, seed: Seed<impl Name>)
    -> ExistLessThanEq<impl HasType<u32>, impl HasType<u32>>
{
    let (seed1, seed2) = seed.replicate();
    if x <= y {
        ExistLessThanEq {
            z: seed1.new_named(x),
            y: seed2.new_named(y),
            less_than_eq: LessThanEq::new(),
        }
    } else {
        ExistLessThanEq {
            z: seed1.new_named(y),
            y: seed2.new_named(y),
            less_than_eq: LessThanEq::new(),
        }
    }
}

Note that I have to repeat x <= y comparison here.

I'm not quite familiar with dependently typed programing, but I believe there should be something better. Do you have any suggestions?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant