#![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(PhantomData); struct Nil(PhantomData); impl Typed for Nil { type Type = ListType; } struct Cons(PhantomData, PhantomData); impl, XS: Typed>> Typed for Cons { type Type = ListType; } trait First: Typed> { type X: Typed; } impl, XS: Typed>> First for Cons { type X = X; } trait ListConcat { type C: Typed>; } impl>> ListConcat for (Nil, X) { type C = X; } impl, As: Typed>, Bs: Typed>> ListConcat for (Cons, Bs) where (As, Bs): ListConcat { type C = Cons>::C>; } trait ListConcatAll: Typed>> { type L: Typed>; } impl ListConcatAll for Nil> { type L = Nil; } impl>, Rest: Typed>>> ListConcatAll for Cons where Rest: ListConcatAll, (Chunk, >::L): ListConcat { type L = <(Chunk, >::L) as ListConcat>::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 B: Typed; } impl Not for True { type B = False; } impl Not for False { type B = True; } trait Or { type B: Typed; } 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 T: Typed; } impl AnyTrue for Nil { type T = False; } impl>> AnyTrue for Cons { type T = True; } impl AnyTrue for Cons where List: AnyTrue { type T = ::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 N: Typed; } 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; } impl PeanoEqual for (N0, N0) { type T = True; } impl> PeanoEqual for (N, N0) { type T = False; } impl> PeanoEqual for (N0, N) { type T = False; } impl, SB: Succ> PeanoEqual for (SA, SB) where (A, B): PeanoEqual { type T = <(A, B) as PeanoEqual>::T; } trait PeanoLT { type T: Typed; } impl PeanoLT for (N0, N0) { type T = False; } impl> PeanoLT for (SX, N0) { type T = False; } impl> PeanoLT for (N0, SX) { type T = True; } impl, SB: Succ> PeanoLT for (SA, SB) where (A, B): PeanoLT { type T = <(A, B) as PeanoLT>::T; } trait PeanoAbsDiff { type C: Typed; } impl PeanoAbsDiff for (N0, N0) { type C = N0; } impl> PeanoAbsDiff for (N0, SB) { type C = SB; } impl> PeanoAbsDiff for (SA, N0) { type C = SA; } impl, SB: Succ> PeanoAbsDiff for (SA, SB) where (A, B): PeanoAbsDiff { type C = <(A, B) as PeanoAbsDiff>::C; } trait Range: Typed { type Xs: Typed>; } impl Range for N0 { type Xs = Nil; } impl> Range for SN where N: Range { type Xs = Cons; } fn accepts_true(_: True) {} fn legal_compare(x: <(N1, N1) as PeanoEqual>::T) { accepts_true(x) } struct Fn1Type(PhantomData, PhantomData); trait Apply { type R: Typed; } struct Conj1>, T>(PhantomData); impl>> Typed for Conj1 { type Type = Fn1Type>; } impl>, X: Typed> Apply> for (Conj1, X) { type R = Cons; } trait Map { type Ys: Typed>; } impl>> Map for (F, Nil) { type Ys = Nil; } impl>, X: Typed, Xs: Typed>> Map for (F, Cons) where (F, X): Apply, (F, Xs): Map { type Ys = Cons<<(F, X) as Apply>::R, <(F, Xs) as Map>::Ys>; } trait MapCat { type Zs: Typed>; } impl>>> MapCat for (F, Nil) { type Zs = Nil; } impl>>, Xs: Typed>> MapCat for (F, Xs) where (F, Xs): Map>, <(F, Xs) as Map>>::Ys: ListConcatAll { type Zs = <<(F, Xs) as Map>>::Ys as ListConcatAll>::L; } trait AppendIf { type Zs: Typed>; } impl, Ys: Typed>> AppendIf for (True, X, Ys) { type Zs = Cons; } impl, Ys: Typed>> AppendIf for (False, X, Ys) { type Zs = Ys; } trait Filter { type Ys: Typed>; } impl>> Filter for (F, Nil) { type Ys = Nil; } impl>, X: Typed, Xs: Typed>> Filter for (F, Cons) where (F, X): Apply, (F, Xs): Filter, (<(F, X) as Apply>::R, X, <(F, Xs) as Filter>::Ys): AppendIf { type Ys = <(<(F, X) as Apply>::R, X, <(F, Xs) as Filter>::Ys) as AppendIf>::Zs; } struct QueenType; struct Queen, Y: Typed>(PhantomData, PhantomData); impl Typed for Queen { type Type = QueenType; } struct Queen1>(PhantomData); impl Typed for Queen1 { type Type = Fn1Type; } impl, Y: Typed> Apply for (Queen1, Y) { type R = Queen; } trait QueensInRow { type Queens: Typed>; } impl, X: Typed> QueensInRow for (N, X) where N: Range, (Queen1, ::Xs): Map { type Queens = <(Queen1, ::Xs) as Map>::Ys; } trait Threatens { type T: Typed; } impl, Ay: Typed, Bx: Typed, By: Typed> Threatens for (Queen, Queen) 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>(PhantomData); impl Typed for Threatens1 { type Type = Fn1Type; } impl, B: Typed> Apply for (Threatens1 , B) where (A, B): Threatens { type R = <(A, B) as Threatens>::T; } trait Safe { type T: Typed; } impl>, Queen: Typed> Safe for (Config, Queen) where (Threatens1, Config): Map, <(Threatens1, Config) as Map>::Ys: AnyTrue, <<(Threatens1, Config) as Map>::Ys as AnyTrue>::T: Not { type T = <<<(Threatens1, Config) as Map>::Ys as AnyTrue>::T as Not>::B; } struct Safe1>>(PhantomData); impl>, Queen> Apply for (Safe1, Queen) where (Config, Queen): Safe { type R = <(Config, Queen) as Safe>::T; } trait AddQueen { type Cs: Typed>; } impl, X: Typed, C: Typed>> AddQueen for (N, X, C) where (N, X): QueensInRow, (Safe1, <(N, X) as QueensInRow>::Queens): Filter, <(Conj1, (Safe1, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys: Map { type Cs = <<(Conj1, (Safe1, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys as Map>::Ys; } struct AddQueen2, X: Typed>(PhantomData, PhantomData); impl, X: Typed> Typed for AddQueen2 { type Type = Fn1Type, ListType>; } impl, X: Typed, C: Typed>> Apply> for (AddQueen2, C) where (N, X, C): AddQueen { type R = <(N, X, C) as AddQueen>::Cs; } trait AddQueenToAll { type CsPrime: Typed>>; } impl, X: Typed, Cs: Typed>>> AddQueenToAll for (N, X, Cs) where (AddQueen2, Cs): MapCat> { type CsPrime = <(AddQueen2, Cs) as MapCat>>::Zs; } trait AddQueensIf { type CsPrime: Typed>>; } impl, Cs: Typed>>> AddQueensIf for (N, N0, Cs) { type CsPrime = Cs; } impl, X: Typed, Cs: Typed>>, SX: Succ> 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>>; } impl, X: Typed, Cs: Typed>>> AddQueens for (N, X, Cs) where (N, X, Cs): AddQueensIf { type CsPrime = <(N, X, Cs) as AddQueensIf>::CsPrime; } trait Solution { type C: Typed>; } impl> Solution for N where (N, N, Cons, Nil>>): AddQueens, <(N, N, Cons, Nil>>) as AddQueens>::CsPrime: First> { type C = <<(N, N, Cons, Nil>>) as AddQueens>::CsPrime as First>>::X; } fn solve() -> ::C { todo!() } fn main() { // we should be able to read the type off the error here let _: () = solve(); }