# Crate refl [−] [src]

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; pub struct Id<S: ?Sized, T: ?Sized>(PhantomData<(*mut S, *mut 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 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

extern crate refl; use refl::*; trait Ty { type Repr: Copy + ::std::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<Expr<T>>, Box<Expr<T>>), } fn eval<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) => 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 |

## Functions

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