KisaragiEffective / origlang

Other
3 stars 0 forks source link

篩型 #160

Open KisaragiEffective opened 1 year ago

KisaragiEffective commented 1 year ago

動機

構文案

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)

概要

述語

以下の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 commented 1 year ago

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

KisaragiEffective commented 1 year ago

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

KisaragiEffective commented 1 year ago

https://github.com/rust-lang/rust/pull/107941