Crate refl

Provides a refl encoding which you can use to provide a proof witness that one type is equivalent (identical) to another type. This can be used to encode a subset of what GADTs allow you to in Haskell.

This is encoded as:

use core::mem;
use core::marker::PhantomData;

pub struct Id<S: ?Sized, T: ?Sized>(PhantomData<(fn(S) -> S, fn(T) -> T)>);

impl<T: ?Sized> Id<T, T> { pub const REFL: Self = Id(PhantomData); }

pub fn refl<T: ?Sized>() -> Id<T, T> { Id::REFL }

impl<S: ?Sized, T: ?Sized> Id<S, T> {
    /// Casts a value of type `S` to `T`.
    ///
    /// This is safe because the `Id` type is always guaranteed to
    /// only be inhabited by `Id<T, T>` types by construction.
    pub fn cast(self, value: S) -> T where S: Sized, T: Sized {
        unsafe {
            // Transmute the value;
            // This is safe since we know by construction that
            // S == T (including lifetime invariance) always holds.
            let cast_value = mem::transmute_copy(&value);

            // Forget the value;
            // otherwise the destructor of S would be run.
            mem::forget(value);

            cast_value
        }
    }

    // ..
}

In Haskell, the Id<A, B> type corresponds to:

data a :~: b where
    Refl :: a :~: a

However, note that you must do the casting manually with refl.cast(val). Rust will not know that S == T by just pattern matching on Id<S, T> (which you cannot do).

Limitations

Please note that Rust has no concept of higher kinded types (HKTs) and so we can not provide the general transformation F<S> -> F<T> given that S == T. With the introduction of generic associated types (GATs), it may be possible to introduce more transformations.

Example - A GADT-encoded expression type

use refl::*;

trait Ty { type Repr: Copy + core::fmt::Debug; }

#[derive(Debug)]
struct Int;
impl Ty for Int { type Repr = usize; }

#[derive(Debug)]
struct Bool;
impl Ty for Bool { type Repr = bool; }

#[derive(Debug)]
enum Expr<T: Ty> {
    Lit(T::Repr),
    Add(Id<usize, T::Repr>, Box<Expr<Int>>, Box<Expr<Int>>),
    If(Box<Expr<Bool>>, Box<Self>, Box<Self>),
}

fn eval<T: Ty>(expr: &Expr<T>) -> T::Repr {
    match expr {
        Expr::Lit(val) => *val,
        Expr::Add(refl, l, r) => refl.cast(eval(l) + eval(r)),
        Expr::If(c, i, e) => if eval(c) { eval(i) } else { eval(e) },
    }
}

fn main() {
    let expr: Expr<Int> =
        Expr::If(
            Box::new(Expr::Lit(false)),
            Box::new(Expr::Lit(1)),
            Box::new(Expr::Add(
                refl(),
                Box::new(Expr::Lit(2)),
                Box::new(Expr::Lit(3)),
            ))
        );

    assert_eq!(eval(&expr), 5);
}

Structs

Id

A proof term that S and T are the same type (type identity). This type is only ever inhabited when S is nominally equivalent to T.

Functions

refl

Construct a proof witness of the fact that a type is equivalent to itself.