mwchase icon

Never has the adjective "uninhabitable" been more fitting

mwchase | PRO | 07/14/17 02:51:02 AM UTC | 0 ⭐ | 821 👁️ | Never ⏰ | []
Rust |

1.2 KB

|

None

|

0 👍

/

0 👎

fn main() {
    println!("{}", (1, (2, Empty())).get::<Succ<Zero>>());
}
 
struct Empty ();
 
trait Cons {
    type Head;
    type Tail: Cons;
    
    fn get_head(&self) -> &Self::Head;
    fn get_tail(&self) -> &Self::Tail;
    
    fn get<T: Peano<Self>>(&self) -> &T::Type where Self: std::marker::Sized {
        T::get(self)
    }
}
 
impl<A, B:Cons> Cons for (A, B) {
    type Head = A;
    type Tail = B;
    
    fn get_head(&self) -> &Self::Head {
        &self.0
    }
    fn get_tail(&self) -> &Self::Tail {
        &self.1
    }
}
 
impl Cons for Empty {
    type Head = Empty;
    type Tail = Empty;
    
    fn get_head(&self) -> &Self::Head {
        panic!()
    }
    fn get_tail(&self) -> &Self::Tail {
        panic!()
    }
}
 
enum Zero {}
 
trait Peano<T: Cons> {
    type Type;
    
    fn get(cons: &T) -> &Self::Type;
}
 
impl<C: Cons> Peano<C> for Zero {
    type Type = C::Head;
    
    fn get(cons: &C) -> &Self::Type {
        cons.get_head()
    }
}
 
struct Succ<T>(T);
 
impl<C: Cons, T: Peano<C::Tail>> Peano<C> for Succ<T> {
    type Type = T::Type;
    
    fn get(cons: &C) -> &Self::Type {
        T::get(cons.get_tail())
    }
}

Comments