hehehehehe

Turing complete compile-time type unification in Rust - demo

#!/bin/rust-script

/// This program uses the Rust type system to solve CCC '20 J1. Rust's type system is Turing complete
/// (see prior art using the SKI calculus [here](https://github.com/Dev380/rust-types-turing-complete)) because
/// solving generic type constraints is isomorphic to reductions in prolog, which is turing complete (in fact
/// the rust type team is rewriting prolog in Rust right now to make the type solver faster). The basic idea
/// is to have a generic type be the input to a function and an associated type be an output. In practice, this
/// means creating a trait for type functions of a particular arity and implementing it for each function type,
/// then casting like so: `<SpecificFunction as FunctionType<ArgumentType>>::Output` to get the output type.
/// Surprisingly, this is only mildly annoying to program it (barring syntax and boilerplate pains), feeling like
/// a primitive untyped functional programming language (although imperative languages like Brainfuck have been written in the type system).
/// The untyped part is very helpful because if too many trait constraints are used (e.g. `Arg: Num, Output: Num` or something like that) the
/// type checker complains, but since all this is happening at compile time the "type system calculus" does not need to have types
/// (runtime error for type programs = compile time error for normal users).
///
/// Note - type arithmetic is an actual useful thing in Rust because generic arrays are taking forever to stabilize,
/// but they use binary instead of peano to avoid the recursion limit of 200 (and for speed)

use std::marker::PhantomData;
use std::fmt::{self, Display, Formatter};

/// Zero - the first number
#[derive(Debug)]
struct Zero;
/// A successor of another number
/// The successor of a number is equal to PlusOne(n) - in normal notation this would be S(n)
#[derive(Debug)]
struct PlusOne<Previous: Reify>(PhantomData<Previous>);

/// The arity-1 function trait
trait Function<Arg> {
	type Output: Reify;
}

/// The arity-2 function trait - a puritan can omit this and use currying
trait BinaryOp<Arg1, Arg2> {
	type Output: Reify;
}

/// The addition function (all functions are unit structs because these are pure functions and the input comes from the trait impl)
#[derive(Debug)]
struct Add;

/// Implement addition for the special cases where one of the inputs are zero
/// and recursively build on that using the peano axiom of a + S(b) = S(a + b)
impl BinaryOp<Zero, Zero> for Add {
	type Output = Zero;
}

/// If PlusOne is not the parameter and a generic argument was used instead, this would conflict with
/// the implementation of BinaryOp<Zero, Zero>
impl<Prev: Reify> BinaryOp<PlusOne<Prev>, Zero> for Add {
	type Output = PlusOne<Prev>;
}

impl<Prev: Reify> BinaryOp<Zero, PlusOne<Prev>> for Add {
	type Output = PlusOne<Prev>;
}

/// Implement the a + S(b) = S(a + b) axiom
impl<Prev1: Reify, Prev2: Reify> BinaryOp<PlusOne<Prev1>, PlusOne<Prev2>> for Add
where Add: BinaryOp<PlusOne<Prev1>, Prev2>
{
	type Output = PlusOne<<Add as BinaryOp<PlusOne<Prev1>, Prev2>>::Output>;
}

/// The multiplication function (defined using peano axioms are before)
#[derive(Debug)]
struct Multiply;

/// a * 0 = 0 axiom
impl BinaryOp<Zero, Zero> for Multiply {
	type Output = Zero;
}

impl<Prev: Reify> BinaryOp<PlusOne<Prev>, Zero> for Multiply {
	type Output = Zero;
}

impl<Prev: Reify> BinaryOp<Zero, PlusOne<Prev>> for Multiply {
	type Output = Zero;
}

/// as before, a recursive peano definition a * S(b) = a + (a * b)
impl<Prev1: Reify, Prev2: Reify> BinaryOp<PlusOne<Prev1>, PlusOne<Prev2>> for Multiply
where
Multiply: BinaryOp<PlusOne<Prev1>, Prev2>,
Add: BinaryOp<PlusOne<Prev1>, <Multiply as BinaryOp<PlusOne<Prev1>, Prev2>>::Output>
{
	type Output = <Add as BinaryOp<PlusOne<Prev1>, <Multiply as BinaryOp<PlusOne<Prev1>, Prev2>>::Output>>::Output;
}

/// The less than a number function - this one has a type parameter because it's actually used as a type parameter for once and not as state or anything
struct LessThanNum<Num: Reify>(PhantomData<Num>);

/// Nothing is less than zero (also a peano axiom I think lol)
impl<Arg: Reify> Function<Arg> for LessThanNum<Zero> {
	type Output = False;
}

/// If something plus one is this number, or is less than this number minus one, then it is less than this number
impl<Arg: Reify, Prev: Reify> Function<Arg> for LessThanNum<PlusOne<Prev>>
where
LessThanNum<Prev>: Function<Arg>,
Equal: BinaryOp<Arg, Prev>,
<Equal as BinaryOp<Arg, Prev>>::Output: BinaryOp<True, <LessThanNum<Prev> as Function<Arg>>::Output>
{
	type Output = <<Equal as BinaryOp<PlusOne<Arg>, PlusOne<Prev>>>::Output as BinaryOp<True, <LessThanNum<Prev> as Function<Arg>>::Output>>::Output;
}

/// True - a function that takes in two arguments and returns the first one
/// (this was useful in making me realize why Church defined booleans like this)
#[derive(Debug)]
struct True;
/// False - True but it returns the second one
#[derive(Debug)]
struct False;

/// Returning arg 1
impl<Arg1: Reify, Arg2: Reify> BinaryOp<Arg1, Arg2> for True {
	type Output = Arg1;
}

/// Returning arg 2
impl<Arg1: Reify, Arg2: Reify> BinaryOp<Arg1, Arg2> for False {
	type Output = Arg2;
}

/// Equality function (peano defines these as same number of successors)
#[derive(Debug)]
struct Equal;

/// Base cases of nothing positive is zero
impl<Prev1: Reify> BinaryOp<PlusOne<Prev1>, Zero> for Equal {
	type Output = False;
}

impl<Prev2: Reify> BinaryOp<Zero, PlusOne<Prev2>> for Equal {
	type Output = False;
}

/// Base case of zero is zero
impl BinaryOp<Zero, Zero> for Equal {
	type Output = True;
}

/// Check equality of "unwrapping" one layer of successors until reaching the base case
impl<Prev1: Reify, Prev2: Reify> BinaryOp<PlusOne<Prev1>, PlusOne<Prev2>> for Equal
where Equal: BinaryOp<Prev1, Prev2>
{
	type Output = <Equal as BinaryOp<Prev1, Prev2>>::Output;
}

/// Convert a type number to an actual number
trait Reify {
	fn to_num() -> u32;
}

impl Reify for Zero {
	fn to_num() -> u32 {
		0
	}
}

impl<Previous: Reify> Reify for PlusOne<Previous> {
	fn to_num() -> u32 {
		Previous::to_num() + 1
	}
}

impl Reify for True {
	fn to_num() -> u32 {
		1
	}
}

impl Reify for False {
	fn to_num() -> u32 {
		0
	}
}

/// Convenience functions for adding and multiplying without all the boilerplate
type QuickAdd<Arg1, Arg2> = <Add as BinaryOp<Arg1, Arg2>>::Output;
type QuickMultiply<Arg1, Arg2> = <Multiply as BinaryOp<Arg1, Arg2>>::Output;

type One = PlusOne<Zero>;
type Two = PlusOne<One>;
type Three = PlusOne<Two>;
type Four = PlusOne<Three>;
type Five = PlusOne<Four>;
type Six = PlusOne<Five>;
type Seven = PlusOne<Six>;
type Eight = PlusOne<Seven>;
type Nine = PlusOne<Eight>;
type Ten = PlusOne<Nine>;

/// Sad and happy - so we can convert to strings and do if-else in the type system instead of at runtime
#[derive(Debug)]
struct Sad;
#[derive(Debug)]
struct Happy;

impl Sad {
	fn new() -> Self {
		Self
	}
}

impl Happy {
	fn new() -> Self {
		Self
	}
}

impl Display for Sad {
	fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
		write!(f, "sad")
	}
}

impl Display for Happy {
	fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
		write!(f, "happy")
	}
}

impl Reify for Sad {
	fn to_num() -> u32 {
		0
	}
}

impl Reify for Happy {
	fn to_num() -> u32 {
		0
	}
}

fn main() -> Result<(), Box<dyn std::error::Error>> {
	type Small = Three;
	type Medium = One;
	type Large = Zero;

	type TwoTimesMedium = QuickMultiply::<Medium, Two>;
	type ThreeTimesLarge = QuickMultiply::<Large, Three>;

	type Happiness = QuickAdd::<Small, QuickAdd::<TwoTimesMedium, ThreeTimesLarge>>;

	type IsSad = <LessThanNum<Ten> as Function<Happiness>>::Output;

	type FinalResult = <IsSad as BinaryOp<Sad, Happy>>::Output;
	
	println!("{} (score: {} = {} + 2 * {} + 3 * {})", FinalResult::new(), Happiness::to_num(), Small::to_num(), Medium::to_num(), Large::to_num());

	Ok(())
}