Last active
August 29, 2018 08:53
-
-
Save konn/f43a3ed710f61e17d12d64d979a292ab to your computer and use it in GitHub Desktop.
Type-level Peano numerals and sized vectors in Rust (Just for fun)
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; | |
pub trait Nat { | |
type Eval; | |
fn as_int() -> usize; | |
} | |
#[derive(Debug)] | |
pub struct Zero {} | |
impl Nat for Zero { | |
type Eval = Zero; | |
fn as_int() -> usize { | |
0 | |
} | |
} | |
#[derive(Debug)] | |
pub struct MkSucc<T> { | |
_maker: PhantomData<fn() -> T>, | |
} | |
impl<T: Nat> Nat for MkSucc<T> { | |
type Eval = MkSucc<<T as Nat>::Eval>; | |
fn as_int() -> usize { | |
1 + <T as Nat>::as_int() | |
} | |
} | |
pub type Succ<T> = <MkSucc<T> as Nat>::Eval; | |
pub struct MkPlus<L, R> { | |
_maker: PhantomData<fn() -> (L, R)>, | |
} | |
impl<R: Nat> Nat for MkPlus<Zero, R> { | |
type Eval = <R as Nat>::Eval; | |
fn as_int() -> usize { | |
<R as Nat>::as_int() | |
} | |
} | |
impl<L, R> Nat for MkPlus<MkSucc<L>, R> | |
where | |
L: Nat, | |
R: Nat, | |
MkPlus<L, R>: Nat, | |
{ | |
type Eval = <MkSucc<MkPlus<L, R>> as Nat>::Eval; | |
fn as_int() -> usize { | |
<MkSucc<L> as Nat>::as_int() + <R as Nat>::as_int() | |
} | |
} | |
pub type Plus<L, R> = <MkPlus<L, R> as Nat>::Eval; | |
pub type One = Succ<Zero>; | |
pub type Two = Plus<One, One>; | |
pub type Three = Succ<Two>; | |
pub type Four = Plus<Two, Two>; | |
pub type Five = Plus<Three, Two>; | |
#[derive(Debug)] | |
pub struct Sized<N, T> { | |
_maker: PhantomData<Fn() -> N>, | |
_vector: Vec<T>, | |
} | |
impl<N: Nat, T> Sized<N, T> { | |
pub fn new(v: Vec<T>) -> Option<Sized<N, T>> { | |
if <N as Nat>::as_int() != v.len() { | |
return None; | |
} else { | |
Some(Sized { | |
_maker: PhantomData, | |
_vector: v, | |
}) | |
} | |
} | |
pub fn size(&self) -> usize { | |
<N as Nat>::as_int() | |
} | |
} | |
impl<T> Sized<Zero, T> { | |
pub fn empty() -> Self { | |
Sized { | |
_vector: vec![], | |
_maker: PhantomData, | |
} | |
} | |
} | |
impl<T> Sized<One, T> { | |
pub fn singleton(x: T) -> Self { | |
Sized { | |
_vector: vec![x], | |
_maker: PhantomData, | |
} | |
} | |
} | |
pub struct MkMult<N, M> { | |
_maker: PhantomData<Fn() -> (N, M)>, | |
} | |
impl<N: Nat> Nat for MkMult<Zero, N> { | |
type Eval = Zero; | |
fn as_int() -> usize { | |
0 | |
} | |
} | |
impl<N, M> Nat for MkMult<MkSucc<N>, M> | |
where | |
N: Nat, | |
M: Nat, | |
MkPlus<M, MkMult<N, M>>: Nat, | |
{ | |
type Eval = <MkPlus<M, MkMult<N, M>> as Nat>::Eval; | |
fn as_int() -> usize { | |
<MkSucc<N> as Nat>::as_int() * <M as Nat>::as_int() | |
} | |
} | |
type Mult<N, M> = <MkMult<N, M> as Nat>::Eval; | |
pub fn append<N, M, T>(l: Sized<N, T>, r: Sized<M, T>) -> Sized<Plus<N, M>, T> | |
where | |
MkPlus<N, M>: Nat, | |
{ | |
let Sized { _vector: mut l, .. } = l; | |
let Sized { _vector: mut r, .. } = r; | |
l.append(&mut r); | |
Sized { | |
_vector: l, | |
_maker: PhantomData, | |
} | |
} | |
pub fn flatten<N, M, T>(vs: Sized<N, Sized<M, T>>) -> Sized<Mult<N, M>, T> | |
where | |
MkMult<N, M>: Nat, | |
{ | |
let Sized { _vector: vs, .. } = vs; | |
let v: Vec<_> = vs.into_iter().flat_map(|a| a._vector.into_iter()).collect(); | |
Sized { | |
_vector: v, | |
_maker: PhantomData, | |
} | |
} | |
impl<N, T> IntoIterator for Sized<N, T> { | |
type Item = <Vec<T> as IntoIterator>::Item; | |
type IntoIter = <Vec<T> as IntoIterator>::IntoIter; | |
fn into_iter(self) -> Self::IntoIter { | |
self._vector.into_iter() | |
} | |
} | |
pub trait Add { | |
type Eval; | |
} | |
impl<N> Add for (Zero, N) { | |
type Eval = N; | |
} |
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
extern crate type_naturals; | |
use type_naturals::*; | |
fn main() { | |
let mfive: Option<Sized<Five, _>> = Sized::new(vec![1, 2, 3, 4, 5]); | |
println!("Sized<Five, _> = {:?}", mfive); | |
let mthree: Option<Sized<Three, _>> = Sized::new(vec![6, 7, 8]); | |
println!("Sized<Three, _> = {:?}", mthree); | |
if let Some(five) = mfive { | |
if let Some(three) = mthree { | |
let eight = append::<Five, Three, _>(five, three); | |
// The followings don't compile... Why?: | |
// let eight = append(five, three); | |
// let eight: Sized<Plus<Four, Four>, _> = append(five, three); | |
println!("Five + Three = {:?}, of size {}", eight, eight.size()); | |
} | |
} | |
println!("Must be None: {:?}", Sized::<Five, ()>::new(vec![])); | |
let nested: Sized<Three, Sized<Four, _>> = Sized::new(vec![ | |
Sized::new(vec![1, 2, 3, 4]).unwrap(), | |
Sized::new(vec![5, 6, 7, 8]).unwrap(), | |
Sized::new(vec![9, 10, 11, 12]).unwrap(), | |
]).unwrap(); | |
println!("Flatting {:?} of size {} to...", nested, nested.size()); | |
let fla = flatten::<Three, Four, _>(nested); | |
// let fla = flatten(nested); | |
println!("...flattened into {:?}, with length {}", fla, fla.size()); | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment