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 mem;
use PhantomData;
>);
Sized>
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 *;
;
;
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.