Diffstat (limited to 'src/any/type_name.rs')
| -rw-r--r-- | src/any/type_name.rs | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/src/any/type_name.rs b/src/any/type_name.rs new file mode 100644 index 0000000..4542b9d --- /dev/null +++ b/src/any/type_name.rs @@ -0,0 +1,100 @@ +//! Bijective mapping between types with and without lifetimes. +//! +//! Types that implement [`Static`] contain no lifetimes (other than `'static`). +//! Types that implement [`WithLt`] contain zero, one, or two lifetimes. +//! The [`Raised`] and [`Lowered`] type aliases can be used to switch between the +//! type having the lifetimes and the type that doesn't. +//! +//! In type theory terms, [`Static`] types represent type constructors needing +//! the two lifetimes `'lt` and `'ctx` (where `'ctx` outlives `'lt`). +//! [`WithLt`] represents the types that have a type constructor of the [`Static`] +//! form. + +/// Lowers a higher ranked type to one with specific lifetimes. +/// +/// This acts to *add* the `'lt` and `'ctx` lifetime to the type. +/// +/// Note the `Bound` generic exists for implied lifetime bounds to make +/// `'ctx: 'lt` work with Rust's `for<'a>` syntax. +pub trait Lower<'lt, 'ctx: 'lt, Bound>: 'static { + /// The lowered type with lifetimes. + type Lowered: ?Sized + Raise<'lt, 'ctx, &'lt &'ctx (), Raised = Self>; +} + +/// Raises a type to one without lifetimes. +/// +/// This acts to *subtract* the `'lt` and `'ctx` lifetime from the type. +/// +/// Note the `Bound` generic exists for implied lifetime bounds to make +/// `'ctx: 'lt` work with Rust's `for<'a>` syntax. +pub trait Raise<'lt, 'ctx: 'lt, Bound>: 'lt { + /// The raised type without lifetimes. + type Raised: ?Sized + Lower<'lt, 'ctx, &'lt &'ctx (), Lowered = Self>; +} + +/// A type without lifetimes (other than `'static`). +/// +/// These types can be lowered to types with lifetimes using [`Lowered`]. +pub trait Static: 'static + for<'lt, 'ctx> Lower<'lt, 'ctx, &'lt &'ctx ()> {} + +impl<T: ?Sized> Static for T where T: 'static + for<'lt, 'ctx> Lower<'lt, 'ctx, &'lt &'ctx ()> {} + +/// A type with zero, one, or two lifetimes. +/// +/// These types can be raised to types without lifetimes using [`Raised`]. +pub trait WithLt<'lt, 'ctx: 'lt>: Raise<'lt, 'ctx, &'lt &'ctx ()> {} + +impl<'lt, 'ctx: 'lt, T: ?Sized> WithLt<'lt, 'ctx> for T where T: Raise<'lt, 'ctx, &'lt &'ctx ()> {} + +/// Add lifetimes to a type without them. +pub type Lowered<'lt, 'ctx, T> = <T as Lower<'lt, 'ctx, &'lt &'ctx ()>>::Lowered; + +/// Remove lifetimes from a type with them. +pub type Raised<'lt, 'ctx, T> = <T as Raise<'lt, 'ctx, &'lt &'ctx ()>>::Raised; + +fn _is_bijective_raise<'lt, 'ctx: 'lt, T>(x: Lowered<'lt, 'ctx, Raised<'lt, 'ctx, T>>) +where + T: WithLt<'lt, 'ctx>, +{ + // This assignment shows T == Lowered<Raised<T>> + let _y: T = x; +} + +fn _is_bijective_lower<'lt, 'ctx: 'lt, U>(x: Raised<'lt, 'ctx, Lowered<'lt, 'ctx, U>>) +where + U: Static, +{ + // This assignment shows U == Raised<Lowered<U>> + let _y: U = x; +} + +// A = set of Static types +// B = set of lifetime types +// +// We only need one of the functions above to show its a bijection. +// If we go a -> b -> a (a: A, b: B) for any a in A +// then we know that there must only exist cycles of length 2. +// This doesn't not however prove by itself that the b we encountered +// is not reused. For that we must consider that we do b -> a using +// Raised which has no information about the a we came from. +// As such, no other a could exist that uses b in it's cycle. +// This proves the two sets are of equal size and that the Lowered +// and Raised form a bijective mapping both ways. +// +// Impossible: +// +// struct A; +// struct B; +// struct C; +// +// impl<'a, 'b> Lower<'a, 'b, &'a &'b ()> for A { +// type Lowered = B; +// } +// +// impl<'a, 'b> Raise<'a, 'b, &'a &'b ()> for B { +// type Raised = A; +// } +// +// impl<'a, 'b> Lower<'a, 'b, &'a &'b ()> for C { +// type Lowered = B; +// } |