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

篩型 #160

Open
KisaragiEffective opened this issue Jun 4, 2023 · 3 comments
Open

篩型 #160

KisaragiEffective opened this issue Jun 4, 2023 · 3 comments

Comments

@KisaragiEffective
Copy link
Owner

KisaragiEffective commented Jun 4, 2023

動機

  • Rustにおける「追加の制約付き」のnewtypeパターンを言語機能でサポートすることである種の未定義動作や脆弱性や不変条件の破壊を防ぐ。

構文案

refine type X = Y with P
refine(P) type X = Y
refine(P) struct X(Y)
struct X(Y with P)
#[derive(Refined)]
#[refined(try_from = P)]
struct X(Y)

概要

  • 篩型Rというのは、ベースとなる型T及びTに属する値tを制限する述語Pからなる。
  • 述語をエンドユーザーが定義できるようにするとややこしいので当分禁止する。
  • 述語は合成可能である。
    • 当然述語の要求に失敗したときのエラーも合成される。
    • 一部の述語は文字通りの合成ではなく、「フュージョン」される。
  • 述語は弱化することが可能である。
  • Rに対してTの可変参照を要求する行為は安全である。~~可変参照を要求したとき、ラッパーが返される。ラッパーは変更が要求されるたびにPによって現在の値を検証する。~~可変参照が無効になったときにPによって検証され、もし条件を満たしていなければpanicする。または、手動で使うことをやめることもでき、その場合はそのやめたところでPによる検証が走るが、panicする代わりにResultを返す。
    • オーバーヘッドを迂回するために検証されない可変参照を要求することもできるが、可変参照が無効になるまでにPによって満たされる条件を満たさなければ未定義動作になる (Rによって保証される不変条件が壊れるため)。

述語

  • And<P1, P2>: P1とP2を同時に満たす述語。可換だがグラフの探索には時間がかかるかもしれないため可換ではないものとして扱う。
  • Or<P1, P2>: P1とP2のどちらか (あるいは両方) を同時に満たす述語。可換だがグラフの探索には時間がかかるかもしれないため可換ではないものとして扱う。
  • Max<T: Ord, const-or-refined-value V: T>: 最大値をVに制限する。
  • Min<T: Ord, const-or-refined-value V: T>: 最小値をVに制限する。
  • Eq<T: Eq, const-or-refined-value V: T>: Vであることを要求する。
  • Not<T, P: Predicate<T>>: P` が満たされないことを要求する。

以下のRustのenumは、篩型で次のようにも表せる:

#[repr(u8)]
enum Hi {
    One = 1,
    Two = 2,
    Three = 3,
}
#[derive(Refined)]
#[refined(try_from = HiPredicate)]
struct Hi

#[derive(RefinedPredicate)]
struct HiPredicate(Or<Eq<u8, 1>, Or<Eq<u8, 2>, Eq<u8, 3>>>)

NonZeroは次のように表せる:

#[derive(Refined)]
#[refined(try_from = NonZeroPredicate::<T>)]
struct NonZero<T: Eq + HasZero>(T)

#[derive(RefinedPredicate)]
struct NonZeroPredicate<T: Eq + HasZero>(Not<Zero<T>>);

struct Zero<invariance T: Eq + Zero>;

impl<T> RefinedPredicate for Zero<T> {
    fn validate(value: T) -> Result<T, Self::Err> {
        if value != Zero::<T>::zero() { Ok(value) } else { Err(NotZeroError(value)) }
    }
}

struct NotZeroError<T>(T);

参照は次のように表せる (ここでは、ライフタイムの問題を無視していることに注意)

#[derive(Refined)]
#[refined(try_from = NonZeroPredicate::<*const T>)]
struct Ref<covariance 'a, covariance T>(*const T)

#[derive(Refined)]
#[refined(try_from = NonZeroPredicate::<*mut T>)]
struct RefMut<covariance 'a, invariance T>(*mut T)
@KisaragiEffective
Copy link
Owner Author

KisaragiEffective commented Jun 5, 2023

メモ: もし可変参照を安全に露出したい場合、RustのPinよりも強い制約を持ったスマポが必要である (具体的には置き換える操作と生の可変参照を露出する操作、及びチェックされない写像を安全ではないとマークし、チェックされる写像を安全とマークする。そして、有効期限が切れた際に走るデストラクタに置いて述語の検証をするようなスマポ。ただし、デストラクタで失敗するとプロセスが強制終了するしかなくなるのはどうなんだという感じ。)

@KisaragiEffective
Copy link
Owner Author

これは言語機能のビルディングブロックにしたい。strは[u8]だし、StringはVec<u8>。いずれも弱めることは容易いが、逆はそうではない。

@KisaragiEffective
Copy link
Owner Author

rust-lang/rust#107941

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