Created
October 4, 2015 10:40
-
-
Save astahfrom/2706fec50e81a6d9935f to your computer and use it in GitHub Desktop.
Approximating GADTs in Rust.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
use std::marker::PhantomData; | |
type Is<S, T> = Is_<S, T>; | |
#[derive(Clone)] | |
struct Is_ <S, T>(PhantomData<S>, PhantomData<T>); | |
fn refl<T>() -> Is<T, T> { | |
Is_(PhantomData, PhantomData) | |
} | |
impl<S, T> Is_<S, T> { | |
fn coerce (&self, value: T) -> S { | |
unsafe { | |
* std::mem::transmute::<_, Box<_>>(Box::new(value)) | |
} | |
} | |
} | |
#[derive(Clone)] | |
enum Exp<T> { | |
LitInt(Is<T, i64>, i64), | |
LitString(Is<T, String>, String), | |
Add(Is<T, i64>, Box<Exp<i64>>, Box<Exp<i64>>), | |
} | |
impl<T> Exp<T> { | |
fn eval(self) -> T { | |
use Exp::*; | |
match self { | |
LitInt(witness, i) => witness.coerce(i), | |
LitString(witness, s) => witness.coerce(s), | |
Add(witness, bx, by) => { | |
let x = bx.eval(); | |
let y = by.eval(); | |
witness.coerce(x + y) | |
}, | |
} | |
} | |
} | |
#[test] | |
fn it_works() { | |
use Exp::*; | |
let one = LitInt(refl(), 1); | |
assert_eq!(one.clone().eval(), 1); | |
let two = LitInt(refl(), 2); | |
assert_eq!(two.clone().eval(), 2); | |
let exp = Add(refl(), Box::new(one), Box::new(two)); | |
assert_eq!(exp.eval(), 3); | |
let name: Exp<String> = LitString(refl(), "GADTs".to_string()); | |
assert_eq!(name.eval(), "GADTs"); | |
// let wrong = Add(refl(), Box::new(name), Box::new(two)); | |
/* | |
src/lib.rs:66:38: 66:42 error: mismatched types: | |
expected `Exp<i64>`, | |
found `Exp<collections::string::String>` | |
(expected i64, | |
found struct `collections::string::String`) [E0308] | |
src/lib.rs:66 let wrong = Add(refl(), Box::new(name), Box::new(two)); | |
^~~~ | |
*/ | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment