Skip to content

Instantly share code, notes, and snippets.

Embed
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
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.