Playing around with type-level operations in rust

typeops.rs

#![allow(unused)]
#![feature(non_ascii_idents)]
// #![feature(conservative_impl_trait)]

// basic nats, my knowledge
mod nat {
  pub trait Nat { fn to_usize() -> usize; }
  pub struct Zero;
  impl Nat for Zero { fn to_usize() -> usize { 0 } }
  pub struct Succ<N>(pub N);
  impl<N:Nat> Nat for Succ<N> { fn to_usize() -> usize {1+N::to_usize()} }
  pub trait Pred { type Pred; }
  impl<N:Nat> Pred for Succ<N> { type Pred=N; }
  pub trait GreaterThan<N> {}
  impl<N:Nat> GreaterThan<Zero> for Succ<N> {}
  impl<N1:Nat,N2:Nat> GreaterThan<Succ<N2>> for Succ<N1> where
    N1: GreaterThan<N2>
  {}
  pub trait Plus<N:Nat> : Nat { type Result:Nat; }
  impl<N:Nat> Plus<Zero> for N { type Result = N; }
  impl<N1:Nat,N2:Nat,N3:Nat> Plus<Succ<N2>> for N1 where
    N1: Plus<N2,Result=N3>
  { type Result = Succ<N3>; }
}

// from an idris tutorial
mod example1 {
  pub struct True;
  pub struct False;
  pub trait StringOrNat {
    type Out;
  }
  impl StringOrNat for True {
    type Out = &'static str;
  }
  impl StringOrNat for False {
    type Out = usize;
  }
  pub trait LengthOrDouble : StringOrNat {
    fn run(self,x:Self::Out) -> usize;
  }
  impl LengthOrDouble for True {
    fn run(self,x:&'static str) -> usize { x.len() }
  }
  impl LengthOrDouble for False {
    fn run(self,x:usize) -> usize { x + x }
  }
}

// from a dependent types tutorial
mod szlist {
  use nat::*;

  pub struct Nil;
  // note that this `Cons` type does not know its child (Like recursive types)
  pub struct Cons<E,PredN>(E,Box<SzList<E,Sz=PredN>>);

  pub trait SzList<E> {
    type Sz;
    fn push(self,e:E) -> Box<SzList<E,Sz=Succ<Self::Sz>>>;
    // fn pop(self) -> Box<SzList<E,Sz=<Self::Sz as Pred>::Pred>> where Self::Sz:Pred;
  }
  impl<E> SzList<E> for Nil {
    type Sz = Zero;
    fn push(self,e:E) -> Box<SzList<E,Sz=Succ<Self::Sz>>>{unimplemented!()}
    // internal compiler error
    // fn pop(self) -> Box<SzList<E,Sz=<Self::Sz as Pred>::Pred>> where Self::Sz:Pred{unimplemented!()}
  }
  impl<E,N> SzList<E> for Cons<E,N> {
    type Sz = Succ<N>;
    fn push(self,e:E) -> Box<SzList<E,Sz=Succ<Self::Sz>>>{unimplemented!()}
    // fn pop(self) -> Box<SzList<E,Sz=<Self::Sz as Pred>::Pred>> where Self::Sz:Pred{unimplemented!()}
  }
  impl<E,N:Pred> Cons<E,N> {
    fn pop(self) -> Box<SzList<E,Sz=N::Pred>>{unimplemented!()}
  }

  pub fn nil() -> Nil {
    Nil
  }
  pub fn cons<E,L:'static+SzList<E>>(e:E,l:L) -> Cons<E,L::Sz> {
    Cons(e,Box::new(l))
  }
  pub fn push<E,L:'static+SzList<E>>(l:L,e:E) -> Cons<E,L::Sz>{
    Cons(e,Box::new(l))
  }
  pub fn pop<E,N,L:SzList<E>>(l:Cons<E,N>) -> (E,Box<SzList<E,Sz=N>>){
    (l.0,l.1)
  }
}

mod hkt {
  pub trait TypeFn1<E> { type Result; }

  pub enum List<E>{
    Nil, Cons(E,Box<List<E>>)
  }
  pub struct ListConstructor;
  impl<E> TypeFn1<E> for ListConstructor {
    type Result = List<E>;
  }
}

// from an agda tutorial
mod example2 { 
  use nat::*;
  pub trait Even : Nat {}
  pub trait Odd : Nat {}
  impl Even for Zero {}
  impl<N:Even> Even for Succ<Succ<N>> {}
  impl<N:Even> Odd for Succ<N> {}

  pub trait And {}
  impl<A,B> And for (A,B) {}
}

fn main() {
  use nat::*;
  type A = Succ<Succ<Zero>>;
  type B = Succ<Succ<Succ<Zero>>>;
  type C = <A as Plus<B>>::Result;
  let a = A::to_usize();
  let b = B::to_usize();
  let c = C::to_usize();
  assert_eq!(a+b, c);
  println!("{}+{}={}",a,b,c);

  use example1::*;
  println!("len('5')={}",LengthOrDouble::run(True,"5"));
  println!("5x2={}",LengthOrDouble::run(False,5));
  println!("5x2={}",False::run(False,5));
  println!("5x2={}",False.run(5));
  
  use szlist::*;
  let a = nil();
  let b = cons(1,cons(2,nil()));
  // finish when rust compiler bug is fixed!

  use example2::*;
  fn assert_even<N:Even>(n:N) {}
  fn assert_odd<N:Odd>(n:N) {}
  assert_even(Succ(Succ(Succ(Succ(Zero)))));
  assert_odd(Succ(Succ(Succ(Zero))));
  #[allow(non_camel_case_types)]
  fn simp0<φ,ψ>((p,q):(φ,ψ)) -> φ where
    (φ,ψ) : And
  { p }
  #[allow(non_camel_case_types)]
  fn simp1<φ,ψ>((p,q):(φ,ψ)) -> ψ where
    (φ,ψ) : And
  { q }

  use hkt::*;
  type T = usize;
  let a : <ListConstructor as TypeFn1<T>>::Result = List::Cons(1,Box::new(List::Cons(2,Box::new(List::Nil))));
}