Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Playing around with type-level operations in rust
#![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))));
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment