refl

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

This is encoded as:

use std::mem;use std::marker::PhantomData;pubstructId<S: ?Sized,T: ?Sized>(PhantomData<(*mutS,*mutT)>);impl<T: ?Sized>Id<T,T>{pubconstREFL:Self = Id(PhantomData);}pubfnrefl<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.pubfncast(self,value:S) -> TwhereS: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:

dataa:~:bwhereRefl::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 can't 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

externcrate refl;use refl::*;traitTy{typeRepr:Copy + ::std::fmt::Debug;}#[derive(Debug)]structInt;implTyforInt{typeRepr = usize;}#[derive(Debug)]structBool;implTyforBool{typeRepr = bool;}#[derive(Debug)]enumExpr<T:Ty>{Lit(T::Repr),Add(Id<usize,T::Repr>,Box<Expr<Int>>,Box<Expr<Int>>),If(Box<Expr<Bool>>,Box<Expr<T>>,Box<Expr<T>>),}fneval<T:Ty>(expr:&Expr<T>) -> T::Repr{match*expr {Expr::Lit(ref val) =>
*val,Expr::Add(ref refl,ref l,ref r) =>
refl.cast(eval(&*l) + eval(&*r)),Expr::If(ref c,ref i,ref e) =>
ifeval(&*c){eval(&*i)}else{eval(&*e)},}}fnmain(){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);}

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.