Skip to content

Instantly share code, notes, and snippets.

@bodil
Last active February 28, 2021 03:50
  • Star 3 You must be signed in to star a gist
  • Fork 2 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save bodil/a6f61e139fdf892b1a632c55f7cffc8b to your computer and use it in GitHub Desktop.
Simple type level natural numbers in Rust
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub struct True;
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub struct False;
pub trait Bool {
fn new() -> Self;
}
impl Bool for True {
fn new() -> True {
True
}
}
impl Bool for False {
fn new() -> False {
False
}
}
pub trait IsTrue {}
impl IsTrue for True {}
pub trait IsFalse {}
impl IsFalse for False {}
use std::ops::{Add, Sub};
use std::cmp::Ordering;
use std::marker::PhantomData;
use std::fmt;
use bool::*;
pub trait Nat {
fn new() -> Self;
fn as_int() -> usize;
}
#[derive(Copy, Clone, PartialEq, Eq)]
pub struct Zero;
impl Nat for Zero {
fn new() -> Self {
Zero
}
fn as_int() -> usize {
0
}
}
#[derive(Copy, Clone, PartialEq, Eq)]
pub struct Succ<N> {
n: PhantomData<N>,
}
impl<N> Nat for Succ<N>
where
N: Nat,
{
fn new() -> Self {
Succ { n: PhantomData }
}
fn as_int() -> usize {
1 + N::as_int()
}
}
pub trait Pos: Nat {}
impl<N> Pos for Succ<N>
where
N: Nat,
{
}
// Addition
pub type Sum<L, R> = <L as Add<R>>::Output;
impl<N: Nat> Add<N> for Zero {
type Output = N;
fn add(self, n: N) -> Self::Output {
n
}
}
impl<L: Nat, R: Add<L>> Add<R> for Succ<L> where <R as Add<L>>::Output: Nat {
type Output = Succ<<R as Add<L>>::Output>;
fn add(self, _: R) -> Self::Output {
<Self::Output as Nat>::new()
}
}
// Subtraction
pub type Diff<L, R> = <L as Sub<R>>::Output;
impl Sub<Zero> for Zero {
type Output = Self;
fn sub(self, _: Zero) -> Self::Output {
self
}
}
impl<N: Nat> Sub<Zero> for Succ<N> {
type Output = Self;
fn sub(self, _: Zero) -> Self::Output {
self
}
}
impl<L: Nat + Sub<R>, R: Nat> Sub<Succ<R>> for Succ<L> where <L as Sub<R>>::Output: Nat {
type Output = <L as Sub<R>>::Output;
fn sub(self, _: Succ<R>) -> Self::Output {
<Self::Output as Nat>::new()
}
}
pub type Pred<N> = Diff<N, Succ<Zero>>;
// Ordering
pub trait Cmp<Other> {
type Output: Order;
}
pub type Compare<L, R> = <L as Cmp<R>>::Output;
pub trait Order {
fn as_ordering() -> Ordering;
}
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub struct Less;
impl Less {
pub fn new() -> Less {
Less
}
}
impl Order for Less {
fn as_ordering() -> Ordering {
Ordering::Less
}
}
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub struct Equal;
impl Equal {
pub fn new() -> Equal {
Equal
}
}
impl Order for Equal {
fn as_ordering() -> Ordering {
Ordering::Equal
}
}
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub struct Greater;
impl Greater {
pub fn new() -> Greater {
Greater
}
}
impl Order for Greater {
fn as_ordering() -> Ordering {
Ordering::Greater
}
}
impl Cmp<Zero> for Zero {
type Output = Equal;
}
impl<N: Nat> Cmp<Zero> for Succ<N> {
type Output = Greater;
}
impl<N: Nat> Cmp<Succ<N>> for Zero {
type Output = Less;
}
impl<L: Nat + Cmp<R>, R: Nat> Cmp<Succ<R>> for Succ<L> {
type Output = <L as Cmp<R>>::Output;
}
impl<R: Nat> PartialOrd<R> for Zero
where
Zero: Cmp<R> + PartialEq<R>,
{
fn partial_cmp(&self, _: &R) -> Option<Ordering> {
Some(<Zero as Cmp<R>>::Output::as_ordering())
}
}
impl<L: Nat + Cmp<R>, R: Nat> PartialOrd<R> for Succ<L>
where
Succ<L>: PartialEq<R>,
{
fn partial_cmp(&self, _: &R) -> Option<Ordering> {
Some(<L as Cmp<R>>::Output::as_ordering())
}
}
pub trait IsLess<C> {
type Output: Bool;
}
impl<L> IsLess<Less> for L {
type Output = True;
}
impl<L> IsLess<Equal> for L {
type Output = False;
}
impl<L> IsLess<Greater> for L {
type Output = False;
}
pub trait IsEqual<C> {
type Output: Bool;
}
impl<L> IsEqual<Less> for L {
type Output = False;
}
impl<L> IsEqual<Equal> for L {
type Output = True;
}
impl<L> IsEqual<Greater> for L {
type Output = False;
}
pub trait IsGreater<C> {
type Output: Bool;
}
impl<L> IsGreater<Less> for L {
type Output = False;
}
impl<L> IsGreater<Equal> for L {
type Output = False;
}
impl<L> IsGreater<Greater> for L {
type Output = True;
}
pub trait LT<R> {
type Output: Bool;
}
impl<L, R> LT<R> for L
where
L: Cmp<R> + IsLess<Compare<L, R>>,
{
type Output = <L as IsLess<Compare<L, R>>>::Output;
}
pub trait EQ<R> {
type Output: Bool;
}
impl<L, R> EQ<R> for L
where
L: Cmp<R> + IsEqual<Compare<L, R>>,
{
type Output = <L as IsEqual<Compare<L, R>>>::Output;
}
pub trait GT<R> {
type Output: Bool;
}
impl<L, R> GT<R> for L
where
L: Cmp<R> + IsGreater<Compare<L, R>>,
{
type Output = <L as IsGreater<Compare<L, R>>>::Output;
}
pub type Lt<L, R> = <L as LT<R>>::Output;
pub type Eq<L, R> = <L as EQ<R>>::Output;
pub type Gt<L, R> = <L as GT<R>>::Output;
// Literals
pub type N0 = Zero;
pub type N1 = Succ<N0>;
pub type N2 = Succ<N1>;
pub type N3 = Succ<N2>;
pub type N4 = Succ<N3>;
pub type N5 = Succ<N4>;
pub type N6 = Succ<N5>;
pub type N7 = Succ<N6>;
pub type N8 = Succ<N7>;
pub type N9 = Succ<N8>;
impl fmt::Debug for Zero {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(f, "0")
}
}
impl<N: Nat> fmt::Debug for Succ<N> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(f, "{}", Self::as_int())
}
}
// Tests
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn it_works() {
assert_eq!(N0::new() + N0::new(), N0::new());
assert_eq!(N0::new() + N2::new(), N2::new());
assert_eq!(N2::new() + N0::new(), N2::new());
assert_eq!(N2::new() + N2::new(), N4::new());
assert_eq!(N2::new() - N0::new(), N2::new());
assert_eq!(N0::new() - N0::new(), N0::new());
assert_eq!(N6::new() - N4::new(), N2::new());
assert_eq!(
format!("{:?}", N2::new() + N2::new()),
format!("{:?}", N4::new())
);
assert_eq!(Greater::new(), Compare::<N4, N2>::new());
assert_eq!(Less::new(), Compare::<N4, N6>::new());
assert_eq!(Equal::new(), Compare::<N4, N4>::new());
assert_eq!(True, Lt::<N2, N4>::new());
assert_eq!(False, Lt::<N4, N2>::new());
assert_eq!(False, Lt::<N2, N2>::new());
assert_eq!(False, Gt::<N2, N4>::new());
assert_eq!(True, Gt::<N4, N2>::new());
assert_eq!(False, Gt::<N2, N2>::new());
assert_eq!(False, Eq::<N2, N4>::new());
assert_eq!(False, Eq::<N4, N2>::new());
assert_eq!(True, Eq::<N2, N2>::new());
}
}
use std::ops::{Add, Sub};
use std::marker::PhantomData;
use std::fmt;
use num::*;
use bool::*;
#[derive(PartialEq, Eq)]
pub struct SizedVec<N, A> {
len: PhantomData<N>,
vec: Vec<A>,
}
impl<A> SizedVec<Zero, A> {
pub fn new() -> Self {
SizedVec {
len: PhantomData,
vec: vec![],
}
}
}
impl<N, A: fmt::Debug> fmt::Debug for SizedVec<N, A> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
self.vec.fmt(f)
}
}
impl<N: Nat, A> SizedVec<N, A> {
pub fn push(self, a: A) -> SizedVec<Succ<N>, A> {
let mut v = self.vec;
v.push(a);
SizedVec {
len: PhantomData,
vec: v,
}
}
pub fn pop(self) -> (SizedVec<Pred<N>, A>, A)
where
N: Sub<N1>,
{
let mut v = self.vec;
let o = v.pop().unwrap();
(
SizedVec {
len: PhantomData,
vec: v,
},
o,
)
}
pub fn append<M: Nat>(self, other: SizedVec<M, A>) -> SizedVec<Sum<N, M>, A>
where
N: Add<M>,
{
let mut left = self.vec;
let mut right = other.vec;
left.append(&mut right);
SizedVec {
len: PhantomData,
vec: left,
}
}
pub fn get<I: Nat + Cmp<N> + IsLess<<I as Cmp<N>>::Output>>(&self, _: I) -> &A
where
Lt<I, N>: IsTrue,
{
&self.vec[I::as_int()]
}
pub fn len(&self) -> N {
N::new()
}
}
#[macro_export]
macro_rules! svec {
() => { $crate::vec::SizedVec::new() };
( $($x:expr),* ) => {{
$crate::vec::SizedVec::new()$(.push($x))*
}};
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_me() {
let v = svec![1, 2, 3];
assert_eq!(N3::new(), v.len());
assert_eq!(&2, v.get(N1::new()));
assert_eq!((svec![1, 2], 3), v.pop());
let v1 = svec![1, 2, 3];
let v2 = svec![4, 5, 6];
let v3 = v1.append(v2);
assert_eq!(N6::new(), v3.len());
assert_eq!(svec![1, 2, 3, 4, 5, 6], v3);
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment