#type #meta-programming #proofs #logic

no-std same-as

稳定Rust中的类型等价

1个稳定版本

1.0.0 2023年5月12日

#1812数学


rsmonad中使用

LGPL-3.0-or-later

6KB

稳定Rust中的类型等价。

使用

一个演示基本原理的玩具示例

use same_as::SameAs;
trait Eat<T> { fn eat<U: SameAs<T>>(_: U); } // Please don't actually write this
struct MrCreosote;
impl Eat<u8> for MrCreosote { fn eat<U: SameAs<u8>>(_: U) {} }
MrCreosote::eat(0_u8); // wafer-thin type

这不会编译

// ...
struct MrCreosote;
impl Eat<u8> for MrCreosote { fn eat<U: SameAs<u8>>(_: U) {} }
MrCreosote::eat(0_u16); // kaboom

但为什么类型等价是必要的呢?

有时你需要它,而Rust现在无法利用它,例如在Rust中定义Haskell风格的monad

pub trait Monad<A>: SameAs<Self::Constructor<A>> { // <-- Enforces that e.g. for `Maybe<A>`, `Self::Constructor` is effectively just the type constructor `Maybe`.
    type Constructor<B>: Monad<B>; // In this `impl`, `Self` is really `Self<A>`, but we want to make `Self<B>` below.
    fn bind<B, F: Fn(A) -> B>(self, f: F) -> Self::Constructor<B>;
}

所以这会工作

pub enum Maybe<A> { Nothing, Just(A) }
impl<A> Monad<A> for Maybe<A> { type Constructor<B> = Maybe<B>; }

但我们可以证明这不会,因此我们可以安全地在Rust中模拟类型构造函数

pub enum Maybe<A> { Nothing, Just(A) } // deception!  vvvvvv
impl<A> Monad<A> for Maybe<A> { type Constructor<B> = Option<B>; }

无运行时依赖