Type-Level Shenanigans

Ingredients & Cooking it up

WARNING

EVIL HACK AHEAD!

Rust's type system

...is basically a Prolog.

With weird syntax.

Excursion: Prolog

  • declarative
  • logic-based
  • solver creates actual program

Ingredients

  • Zero-Sized Types
  • Traits
  • Generics and Associated Types

Atoms

Zero-Sized structs 

//! Example: Kleene Logic
pub struct True;
pub struct False;
pub struct Unknown;

Operations on Types


impl Not for True {
    type Output = False; // associated Type
    fn not(self) -> Self::Output { unreachable!() }
}
impl Not for False { .. } // Output = True
impl Not for Unknown { .. } // Output = Unknown

Multi-Type Ops


impl<X> BitAnd<X> for True {
    type Output = X; // generic result type
    fn and(self, other: X) -> Self::Output { 
        unreachable!() 
    }
}
impl<X> BitAnd<X> for False {
    type Output = False; // fixed result type
    fn and(self, other: X) -> Self::Output { .. }
}
// non-generic impls for Unknown omitted

Usage


<True as Not>::Output // == False

<X as BitAnd<Y>>::Output // == X ∧ Y

<<X as BitOr<Y>>::Output as Not>::Output // == ¬(X ∨ Y)

Molecules

PhantomData<_>: bind atoms together 

// typenum, src/uint.rs (note the generic types!)
pub struct UInt<U, B> {
    _marker: PhantomData<(U, B)>
}

UInt is zero-sized, but has two component types.

9:  • ←  1 ←  0 ←  0 ←  1 

Related

Same / Cmp

missing impls are type errors


pub trait Same<Rhs = Self> {
    type Output;
}

impl<T> Same<T> for T {
    type Output = T;
}

Evaluate

convert to runtime values 

pub enum Ternary { T, F, U }
pub trait TernaryType {
    fn to_ternary() -> Ternary;
}
impl TernaryType for True {
    #[inline] fn to_ternary() -> Ternary { Ternary::T }
}
...

where clauses


impl<Ul: Unsigned + NonZero, Ur: Unsigned + NonZero> 
        Add<PInt<Ur>> for PInt<Ul> {
    type Output = PInt<<Ul as Add<Ur>>::Output>; // …
}
leads to 

src/uint.rs:241:1: 247:2 error: the trait `core::ops::Add<Ur>`
    is not implemented for the type `Ul` [E0277]
src/uint.rs:241 impl<Ul: Unsigned, Ur: Unsigned> Add<Ul, …

where clauses

Compiler asks for missing trait? Use where. 

/// From typenum's src/int.rs: `P(Ul) + P(Ur) = P(Ul + Ur)`
impl<Ul: Unsigned + NonZero, Ur: Unsigned + NonZero> 
        Add<PInt<Ur>> for PInt<Ul>
    where Ul: Add<Ur>,
          <Ul as Add<Ur>>::Output: Unsigned + NonZero {
    type Output = PInt<<Ul as Add<Ur>>::Output>;
    fn add(self, _: PInt<Ur>) -> Self::Output { .. }
}

where clauses

But: overuse of where clauses can lead to exponential compile time! (#26325)

replace generic impls with (multiple) concrete typed impls

private intermediate traits can help

Testing

Did I mention compiletest is awesome?

Build code and run

See more examples

Questions?