Last active
February 14, 2024 17:44
-
-
Save Dev380/ff52e73e8cd99d2f1724df7597e6e23d to your computer and use it in GitHub Desktop.
hehehehehe
This file contains 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
#!/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