path: root/src/main.rs

#![recursion_limit="500"]

//! [source 1](https://aphyr.com/posts/342-typing-the-technical-interview)
//! [source 2](https://sdleffler.github.io/RustTypeSystemTuringComplete/)
use std::marker::PhantomData;

trait Typed {
    type Type;
}

struct ListType<T>(PhantomData<T>);

struct Nil<T>(PhantomData<T>);
impl<T> Typed for Nil<T> { type Type = ListType<T>; }
struct Cons<X, XS>(PhantomData<X>, PhantomData<XS>);
impl<T, X: Typed<Type=T>, XS: Typed<Type=ListType<T>>> Typed for Cons<X, XS> { type Type = ListType<T>; }

trait First<T>: Typed<Type=ListType<T>> {
    type X: Typed<Type=T>;
}

impl<T, X: Typed<Type=T>, XS: Typed<Type=ListType<T>>> First<T> for Cons<X, XS> {
    type X = X;
}

trait ListConcat<X> {
    type C: Typed<Type=ListType<X>>;
}

impl<T, X: Typed<Type=ListType<T>>> ListConcat<T> for (Nil<T>, X) {
    type C = X;
}

impl<T, A: Typed<Type=T>, As: Typed<Type=ListType<T>>, Bs: Typed<Type=ListType<T>>> ListConcat<T> for (Cons<A, As>, Bs)
    where (As, Bs): ListConcat<T> {
    type C = Cons<A, <(As, Bs) as ListConcat<T>>::C>;
}

trait ListConcatAll<T>: Typed<Type=ListType<ListType<T>>> {
    type L: Typed<Type=ListType<T>>;
}

impl<T> ListConcatAll<T> for Nil<ListType<T>> {
    type L = Nil<T>;
}

impl<T, Chunk: Typed<Type=ListType<T>>, Rest: Typed<Type=ListType<ListType<T>>>> ListConcatAll<T> for Cons<Chunk, Rest>
    where Rest: ListConcatAll<T>, (Chunk, <Rest as ListConcatAll<T>>::L): ListConcat<T> {
    type L = <(Chunk, <Rest as ListConcatAll<T>>::L) as ListConcat<T>>::C;
}

struct BoolType;

struct True;
impl Typed for True { type Type = BoolType; }
struct False;
impl Typed for False { type Type = BoolType; }

trait Not: Typed<Type=BoolType> {
    type B: Typed<Type=BoolType>;
}

impl Not for True {
    type B = False;
}

impl Not for False {
    type B = True;
}

trait Or {
    type B: Typed<Type=BoolType>;
}

impl Or for (True, True) {
    type B = True;
}

impl Or for (True, False) {
    type B = True;
}

impl Or for (False, True) {
    type B = True;
}

impl Or for (False, False) {
    type B = False;
}

trait AnyTrue: Typed<Type=ListType<BoolType>> {
    type T: Typed<Type=BoolType>;
}

impl AnyTrue for Nil<BoolType> {
    type T = False;
}

impl<More: Typed<Type=ListType<BoolType>>> AnyTrue for Cons<True, More> {
    type T = True;
}

impl<List> AnyTrue for Cons<False, List> where List: AnyTrue {
    type T = <List as AnyTrue>::T;
}

struct NatType;

struct N0;
impl Typed for N0 { type Type = NatType; }
struct N1;
impl Typed for N1 { type Type = NatType; }
struct N2;
impl Typed for N2 { type Type = NatType; }
struct N3;
impl Typed for N3 { type Type = NatType; }
struct N4;
impl Typed for N4 { type Type = NatType; }
struct N5;
impl Typed for N5 { type Type = NatType; }
struct N6;
impl Typed for N6 { type Type = NatType; }
struct N7;
impl Typed for N7 { type Type = NatType; }
struct N8;
impl Typed for N8 { type Type = NatType; }

trait Succ: Typed<Type=NatType> {
    type N: Typed<Type=NatType>;
}

impl Succ for N1 { type N = N0; }
impl Succ for N2 { type N = N1; }
impl Succ for N3 { type N = N2; }
impl Succ for N4 { type N = N3; }
impl Succ for N5 { type N = N4; }
impl Succ for N6 { type N = N5; }
impl Succ for N7 { type N = N6; }
impl Succ for N8 { type N = N7; }

trait PeanoEqual {
    type T: Typed<Type=BoolType>;
}

impl PeanoEqual for (N0, N0) {
    type T = True;
}

impl<A, N: Succ<N=A>> PeanoEqual for (N, N0) {
    type T = False;
}

impl<B, N: Succ<N=B>> PeanoEqual for (N0, N) {
    type T = False;
}

impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoEqual for (SA, SB) where (A, B): PeanoEqual {
    type T = <(A, B) as PeanoEqual>::T;
}

trait PeanoLT {
    type T: Typed<Type=BoolType>;
}

impl PeanoLT for (N0, N0) {
    type T = False;
}

impl<X, SX: Succ<N=X>> PeanoLT for (SX, N0) {
    type T = False;
}

impl<X, SX: Succ<N=X>> PeanoLT for (N0, SX) {
    type T = True;
}

impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoLT for (SA, SB) where (A, B): PeanoLT {
    type T = <(A, B) as PeanoLT>::T;
}

trait PeanoAbsDiff {
    type C: Typed<Type=NatType>;
}

impl PeanoAbsDiff for (N0, N0) {
    type C = N0;
}

impl<B, SB: Succ<N=B>> PeanoAbsDiff for (N0, SB) {
    type C = SB;
}

impl<A, SA: Succ<N=A>> PeanoAbsDiff for (SA, N0) {
    type C = SA;
}

impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoAbsDiff for (SA, SB) where (A, B): PeanoAbsDiff {
    type C = <(A, B) as PeanoAbsDiff>::C;
}

trait Range: Typed<Type=NatType> {
    type Xs: Typed<Type=ListType<NatType>>;
}

impl Range for N0 {
    type Xs = Nil<NatType>;
}

impl<N, SN: Succ<N=N>> Range for SN where N: Range {
    type Xs = Cons<N, N::Xs>;
}

fn accepts_true(_: True) {}
fn legal_compare(x: <(N1, N1) as PeanoEqual>::T) {
    accepts_true(x)
}

struct Fn1Type<X, R>(PhantomData<X>, PhantomData<R>);

trait Apply<T> {
    type R: Typed<Type=T>;
}

struct Conj1<List: Typed<Type=ListType<T>>, T>(PhantomData<List>);
impl<T, List: Typed<Type=ListType<T>>> Typed for Conj1<List, T> { type Type = Fn1Type<T, ListType<T>>; }

impl<T, List: Typed<Type=ListType<T>>, X: Typed<Type=T>> Apply<ListType<T>> for (Conj1<List, T>, X) {
    type R = Cons<X, List>;
}

trait Map<T> {
    type Ys: Typed<Type=ListType<T>>;
}

impl<T1, T2, F: Typed<Type=Fn1Type<T1, T2>>> Map<T2> for (F, Nil<T1>) {
    type Ys = Nil<T2>;
}

impl<T1, T2, F: Typed<Type=Fn1Type<T1, T2>>, X: Typed<Type=T1>, Xs: Typed<Type=ListType<T1>>> Map<T2> for (F, Cons<X, Xs>)
    where (F, X): Apply<T2>, (F, Xs): Map<T2> {
    type Ys = Cons<<(F, X) as Apply<T2>>::R, <(F, Xs) as Map<T2>>::Ys>;
}

trait MapCat<T> {
    type Zs: Typed<Type=ListType<T>>;
}

impl<T1, T2, F: Typed<Type=Fn1Type<T1, ListType<T2>>>> MapCat<T2> for (F, Nil<T1>) {
    type Zs = Nil<T2>;
}

impl<T1, T2, F: Typed<Type=Fn1Type<T1, ListType<T2>>>, Xs: Typed<Type=ListType<T1>>> MapCat<T2> for (F, Xs)
    where (F, Xs): Map<ListType<T2>>, <(F, Xs) as Map<ListType<T2>>>::Ys: ListConcatAll<T2> {
    type Zs = <<(F, Xs) as Map<ListType<T2>>>::Ys as ListConcatAll<T2>>::L;
}

trait AppendIf<T> {
    type Zs: Typed<Type=ListType<T>>;
}

impl<T, X: Typed<Type=T>, Ys: Typed<Type=ListType<T>>> AppendIf<T> for (True, X, Ys) {
    type Zs = Cons<X, Ys>;
}

impl<T, X: Typed<Type=T>, Ys: Typed<Type=ListType<T>>> AppendIf<T> for (False, X, Ys) {
    type Zs = Ys;
}

trait Filter<T> {
    type Ys: Typed<Type=ListType<T>>;
}

impl<T, F: Typed<Type=Fn1Type<T, BoolType>>> Filter<T> for (F, Nil<T>) {
    type Ys = Nil<T>;
}

impl<T, F: Typed<Type=Fn1Type<T, BoolType>>, X: Typed<Type=T>, Xs: Typed<Type=ListType<T>>> Filter<T> for (F, Cons<X, Xs>)
    where (F, X): Apply<BoolType>, (F, Xs): Filter<T>,
          (<(F, X) as Apply<BoolType>>::R, X, <(F, Xs) as Filter<T>>::Ys): AppendIf<T> {
    type Ys = <(<(F, X) as Apply<BoolType>>::R, X, <(F, Xs) as Filter<T>>::Ys) as AppendIf<T>>::Zs;
}

struct QueenType;

struct Queen<X: Typed<Type=NatType>, Y: Typed<Type=NatType>>(PhantomData<X>, PhantomData<Y>);
impl<X, Y> Typed for Queen<X, Y> { type Type = QueenType; }
struct Queen1<X: Typed<Type=NatType>>(PhantomData<X>);
impl<X> Typed for Queen1<X> { type Type = Fn1Type<NatType, QueenType>; }

impl<X: Typed<Type=NatType>, Y: Typed<Type=NatType>> Apply<QueenType> for (Queen1<X>, Y) {
    type R = Queen<X, Y>;
}

trait QueensInRow {
    type Queens: Typed<Type=ListType<QueenType>>;
}

impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>> QueensInRow for (N, X)
    where N: Range, (Queen1<X>, <N as Range>::Xs): Map<QueenType> {
    type Queens = <(Queen1<X>, <N as Range>::Xs) as Map<QueenType>>::Ys;
}

trait Threatens {
    type T: Typed<Type=BoolType>;
}

impl<Ax: Typed<Type=NatType>, Ay: Typed<Type=NatType>, Bx: Typed<Type=NatType>, By: Typed<Type=NatType>> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
    where (Ax, Bx): PeanoEqual + PeanoAbsDiff, (Ay, By): PeanoEqual + PeanoAbsDiff,
          (<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T): Or,
          (<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C): PeanoEqual,
          (<(<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T) as Or>::B,
           <(<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C) as PeanoEqual>::T,
          ): Or {
    type T = <(
        <(<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T) as Or>::B,
        <(<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C) as PeanoEqual>::T,
    ) as Or>::B;
}

struct Threatens1<A: Typed<Type=QueenType>>(PhantomData<A>);
impl<A> Typed for Threatens1<A> { type Type = Fn1Type<QueenType, BoolType>; }

impl<A: Typed<Type=QueenType>, B: Typed<Type=QueenType>> Apply<BoolType> for (Threatens1<A>, B)
    where (A, B): Threatens {
    type R = <(A, B) as Threatens>::T;
}

trait Safe {
    type T: Typed<Type=BoolType>;
}

impl<Config: Typed<Type=ListType<QueenType>>, Queen: Typed<Type=QueenType>> Safe for (Config, Queen)
    where (Threatens1<Queen>, Config): Map<BoolType>,
          <(Threatens1<Queen>, Config) as Map<BoolType>>::Ys: AnyTrue,
          <<(Threatens1<Queen>, Config) as Map<BoolType>>::Ys as AnyTrue>::T: Not {
    type T = <<<(Threatens1<Queen>, Config) as Map<BoolType>>::Ys as AnyTrue>::T as Not>::B;
}

struct Safe1<Config: Typed<Type=ListType<QueenType>>>(PhantomData<Config>);

impl<Config: Typed<Type=ListType<QueenType>>, Queen> Apply<BoolType> for (Safe1<Config>, Queen)
    where (Config, Queen): Safe {
    type R = <(Config, Queen) as Safe>::T;
}

trait AddQueen {
    type Cs: Typed<Type=ListType<QueenType>>;
}

impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, C: Typed<Type=ListType<QueenType>>> AddQueen for (N, X, C)
    where (N, X): QueensInRow,
          (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter<QueenType>,
          <(Conj1<C, QueenType>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter<QueenType>>::Ys: Map<QueenType> {
    type Cs = <<(Conj1<C, QueenType>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter<QueenType>>::Ys as Map<QueenType>>::Ys;
}

struct AddQueen2<N: Typed<Type=NatType>, X: Typed<Type=NatType>>(PhantomData<N>, PhantomData<X>);
impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>> Typed for AddQueen2<N, X> { type Type = Fn1Type<ListType<QueenType>, ListType<QueenType>>; }

impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, C: Typed<Type=ListType<QueenType>>> Apply<ListType<QueenType>> for (AddQueen2<N, X>, C)
    where (N, X, C): AddQueen {
    type R = <(N, X, C) as AddQueen>::Cs;
}

trait AddQueenToAll {
    type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
}

impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueenToAll for (N, X, Cs)
    where (AddQueen2<N, X>, Cs): MapCat<ListType<QueenType>> {
    type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat<ListType<QueenType>>>::Zs;
}

trait AddQueensIf {
    type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
}

impl<N: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueensIf for (N, N0, Cs) {
    type CsPrime = Cs;
}

impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>, SX: Succ<N=X>> AddQueensIf for (N, SX, Cs)
    where (N, SX, Cs): AddQueenToAll,
          (N, X, <(N, SX, Cs) as AddQueenToAll>::CsPrime): AddQueens {
    type CsPrime = <(N, X, <(N, SX, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
}

trait AddQueens {
    type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
}

impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueens for (N, X, Cs)
    where (N, X, Cs): AddQueensIf {
    type CsPrime = <(N, X, Cs) as AddQueensIf>::CsPrime;
}

trait Solution {
    type C: Typed<Type=ListType<QueenType>>;
}

impl<N: Typed<Type=NatType>> Solution for N
    where (N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>): AddQueens, <(N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>) as AddQueens>::CsPrime: First<ListType<QueenType>> {
    type C = <<(N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>) as AddQueens>::CsPrime as First<ListType<QueenType>>>::X;
}

fn solve() -> <N6 as Solution>::C {
    todo!()
}

fn main() {
    // we should be able to read the type off the error here
    let _: () = solve();
}