Skip to content

Instantly share code, notes, and snippets.

Show Gist options
  • Save Dev380/ff52e73e8cd99d2f1724df7597e6e23d to your computer and use it in GitHub Desktop.
Save Dev380/ff52e73e8cd99d2f1724df7597e6e23d to your computer and use it in GitHub Desktop.
hehehehehe
#!/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(())
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment