From a07fed3794c0f91b4c2c7cd2332163b8cf031a72 Mon Sep 17 00:00:00 2001
From: Melody Horn <melody@boringcactus.com>
Date: Fri, 12 Mar 2021 18:55:07 -0700
Subject: a first attempt at heresy

---
 src/main.chalk | 336 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/main.rs    | 364 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 700 insertions(+)
 create mode 100644 src/main.chalk
 create mode 100644 src/main.rs

(limited to 'src')

diff --git a/src/main.chalk b/src/main.chalk
new file mode 100644
index 0000000..4837512
--- /dev/null
+++ b/src/main.chalk
@@ -0,0 +1,336 @@
+struct Nil {}
+struct Cons<X, XS> {}
+
+trait First {
+    type X;
+}
+
+impl First for Nil {
+    type X = Nil;
+}
+
+impl<X, XS> First for Cons<X, XS> {
+    type X = X;
+}
+
+trait ListConcat {
+    type C;
+}
+
+impl<X> ListConcat for (Nil, X) {
+    type C = X;
+}
+
+impl<A, As, Bs> ListConcat for (Cons<A, As>, Bs) where (As, Bs): ListConcat {
+    type C = Cons<A, <(As, Bs) as ListConcat>::C>;
+}
+
+trait ListConcatAll {
+    type L;
+}
+
+impl ListConcatAll for Nil {
+    type L = Nil;
+}
+
+impl<Chunk, Rest> ListConcatAll for Cons<Chunk, Rest> where Rest: ListConcatAll, (Chunk, <Rest as ListConcatAll>::L): ListConcat {
+    type L = <(Chunk, <Rest as ListConcatAll>::L) as ListConcat>::C;
+}
+
+struct True {}
+struct False {}
+
+trait Not {
+    type B;
+}
+
+impl Not for True {
+    type B = False;
+}
+
+impl Not for False {
+    type B = True;
+}
+
+trait Or {
+    type B;
+}
+
+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 {
+    type T;
+}
+
+impl AnyTrue for Nil {
+    type T = False;
+}
+
+impl<More> 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 Z {}
+struct S<N> {}
+
+trait PeanoEqual {
+    type T;
+}
+
+impl PeanoEqual for (Z, Z) {
+    type T = True;
+}
+
+impl<A> PeanoEqual for (S<A>, Z) {
+    type T = False;
+}
+
+impl<B> PeanoEqual for (Z, S<B>) {
+    type T = False;
+}
+
+impl<A, B> PeanoEqual for (S<A>, S<B>) where (A, B): PeanoEqual {
+    type T = <(A, B) as PeanoEqual>::T;
+}
+
+trait PeanoLT {
+    type T;
+}
+
+impl PeanoLT for (Z, Z) {
+    type T = False;
+}
+
+impl<X> PeanoLT for (S<X>, Z) {
+    type T = False;
+}
+
+impl<X> PeanoLT for (Z, S<X>) {
+    type T = True;
+}
+
+impl<A, B> PeanoLT for (S<A>, S<B>) where (A, B): PeanoLT {
+    type T = <(A, B) as PeanoLT>::T;
+}
+
+trait PeanoAbsDiff {
+    type C;
+}
+
+impl PeanoAbsDiff for (Z, Z) {
+    type C = Z;
+}
+
+impl<B> PeanoAbsDiff for (Z, S<B>) {
+    type C = S<B>;
+}
+
+impl<A> PeanoAbsDiff for (S<A>, Z) {
+    type C = S<A>;
+}
+
+impl<A, B> PeanoAbsDiff for (S<A>, S<B>) where (A, B): PeanoAbsDiff {
+    type C = <(A, B) as PeanoAbsDiff>::C;
+}
+
+trait Range {
+    type Xs;
+}
+
+impl Range for Z {
+    type Xs = Nil;
+}
+
+impl<N> Range for S<N> where N: Range {
+    type Xs = Cons<N, <N as Range>::Xs>;
+}
+
+trait Apply {
+    type R;
+}
+
+struct Conj1<List> {}
+
+impl<List, X> Apply for (Conj1<List>, X) {
+    type R = Cons<X, List>;
+}
+
+trait Map {
+    type Ys;
+}
+
+impl<F> Map for (F, Nil) {
+    type Ys = Nil;
+}
+
+impl<F, X, Xs> Map for (F, Cons<X, Xs>) where (F, X): Apply, (F, Xs): Map {
+    type Ys = Cons<<(F, X) as Apply>::R, <(F, Xs) as Map>::Ys>;
+}
+
+trait MapCat {
+    type Zs;
+}
+
+impl<F> MapCat for (F, Nil) {
+    type Zs = Nil;
+}
+
+impl<F, Xs> 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;
+}
+
+impl<X, Ys> AppendIf for (True, X, Ys) {
+    type Zs = Cons<X, Ys>;
+}
+
+impl<X, Ys> AppendIf for (False, X, Ys) {
+    type Zs = Ys;
+}
+
+trait Filter {
+    type Ys;
+}
+
+impl<F> Filter for (F, Nil) {
+    type Ys = Nil;
+}
+
+impl<F, X, Xs> Filter for (F, Cons<X, Xs>) 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 Queen<X, Y> {}
+struct Queen1<X> {}
+
+impl<X, Y> Apply for (Queen1<X>, Y) {
+    type R = Queen<X, Y>;
+}
+
+trait QueensInRow {
+    type Queens;
+}
+
+impl<N, X> QueensInRow for (N, X) where N: Range, (Queen1<X>, <N as Range>::Xs): Map {
+    type Queens = <(Queen1<X>, <N as Range>::Xs) as Map>::Ys;
+}
+
+trait Threatens {
+    type T;
+}
+
+impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
+    where (Ax, Bx): PeanoEqual, (Ax, Bx): PeanoAbsDiff, (Ay, By): PeanoEqual, (Ay, By): 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> {}
+
+impl<A, B> Apply for (Threatens1<A>, B) where (A, B): Threatens {
+    type R = <(A, B) as Threatens>::T;
+}
+
+trait Safe {
+    type T;
+}
+
+impl<Config, Queen> Safe for (Config, Queen)
+    where (Threatens1<Queen>, Config): Map,
+          <(Threatens1<Queen>, Config) as Map>::Ys: AnyTrue,
+          <<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T: Not {
+    type T = <<<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T as Not>::B;
+}
+
+struct Safe1<Config> {}
+
+impl<Config, Queen> Apply for (Safe1<Config>, Queen) where (Config, Queen): Safe {
+    type R = <(Config, Queen) as Safe>::T;
+}
+
+trait AddQueen {
+    type Cs;
+}
+
+impl<N, X, C> AddQueen for (N, X, C)
+    where (N, X): QueensInRow,
+          (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter,
+          <(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys: Map {
+    type Cs = <<(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys as Map>::Ys;
+}
+
+struct AddQueen2<N, X> {}
+
+impl<N, X, C> Apply for (AddQueen2<N, X>, C) where (N, X, C): AddQueen {
+    type R = <(N, X, C) as AddQueen>::Cs;
+}
+
+trait AddQueenToAll {
+    type CsPrime;
+}
+
+impl<N, X, Cs> AddQueenToAll for (N, X, Cs) where (AddQueen2<N, X>, Cs): MapCat {
+    type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat>::Zs;
+}
+
+trait AddQueensIf {
+    type CsPrime;
+}
+
+impl<N, X, Cs> AddQueensIf for (False, N, X, Cs) {
+    type CsPrime = Cs;
+}
+
+impl<N, X, Cs> AddQueensIf for (True, N, X, Cs)
+    where (N, X, Cs): AddQueenToAll,
+          (N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime): AddQueens {
+    type CsPrime = <(N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
+}
+
+trait AddQueens {
+    type CsPrime;
+}
+
+impl<N, X, Cs> AddQueens for (N, X, Cs)
+    where (X, N): PeanoLT,
+          (<(X, N) as PeanoLT>::T, N, X, Cs): AddQueensIf {
+    type CsPrime = <(<(X, N) as PeanoLT>::T, N, X, Cs) as AddQueensIf>::CsPrime;
+}
+
+trait Solution {
+    type C;
+}
+
+impl<N> Solution for N where (N, Z, Cons<Nil, Nil>): AddQueens, <(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime: First {
+    type C = <<(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime as First>::X;
+}
+
+// <N6 as Solution>::C
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 0000000..0c96e4e
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,364 @@
+#![recursion_limit="100000"]
+
+//! [source 1](https://aphyr.com/posts/342-typing-the-technical-interview)
+//! [source 2](https://sdleffler.github.io/RustTypeSystemTuringComplete/)
+use std::marker::PhantomData;
+
+struct Nil;
+struct Cons<X, XS>(PhantomData<X>, PhantomData<XS>);
+
+trait First {
+    type X;
+}
+
+impl First for Nil {
+    type X = Nil;
+}
+
+impl<X, XS> First for Cons<X, XS> {
+    type X = X;
+}
+
+trait ListConcat {
+    type C;
+}
+
+impl<X> ListConcat for (Nil, X) {
+    type C = X;
+}
+
+impl<A, As, Bs> ListConcat for (Cons<A, As>, Bs) where (As, Bs): ListConcat {
+    type C = Cons<A, <(As, Bs) as ListConcat>::C>;
+}
+
+trait ListConcatAll {
+    type L;
+}
+
+impl ListConcatAll for Nil {
+    type L = Nil;
+}
+
+impl<Chunk, Rest> ListConcatAll for Cons<Chunk, Rest> where Rest: ListConcatAll, (Chunk, <Rest as ListConcatAll>::L): ListConcat {
+    type L = <(Chunk, <Rest as ListConcatAll>::L) as ListConcat>::C;
+}
+
+struct True;
+struct False;
+
+trait Not {
+    type B;
+}
+
+impl Not for True {
+    type B = False;
+}
+
+impl Not for False {
+    type B = True;
+}
+
+trait Or {
+    type B;
+}
+
+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 {
+    type T;
+}
+
+impl AnyTrue for Nil {
+    type T = False;
+}
+
+impl<More> 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 Z;
+struct S<N>(PhantomData<N>);
+
+type N0 = Z;
+type N1 = S<N0>;
+type N2 = S<N1>;
+type N3 = S<N2>;
+type N4 = S<N3>;
+type N5 = S<N4>;
+type N6 = S<N5>;
+type N7 = S<N6>;
+type N8 = S<N7>;
+
+trait PeanoEqual {
+    type T;
+}
+
+impl PeanoEqual for (Z, Z) {
+    type T = True;
+}
+
+impl<A> PeanoEqual for (S<A>, Z) {
+    type T = False;
+}
+
+impl<B> PeanoEqual for (Z, S<B>) {
+    type T = False;
+}
+
+impl<A, B> PeanoEqual for (S<A>, S<B>) where (A, B): PeanoEqual {
+    type T = <(A, B) as PeanoEqual>::T;
+}
+
+trait PeanoLT {
+    type T;
+}
+
+impl PeanoLT for (Z, Z) {
+    type T = False;
+}
+
+impl<X> PeanoLT for (S<X>, Z) {
+    type T = False;
+}
+
+impl<X> PeanoLT for (Z, S<X>) {
+    type T = True;
+}
+
+impl<A, B> PeanoLT for (S<A>, S<B>) where (A, B): PeanoLT {
+    type T = <(A, B) as PeanoLT>::T;
+}
+
+trait PeanoAbsDiff {
+    type C;
+}
+
+impl PeanoAbsDiff for (Z, Z) {
+    type C = Z;
+}
+
+impl<B> PeanoAbsDiff for (Z, S<B>) {
+    type C = S<B>;
+}
+
+impl<A> PeanoAbsDiff for (S<A>, Z) {
+    type C = S<A>;
+}
+
+impl<A, B> PeanoAbsDiff for (S<A>, S<B>) where (A, B): PeanoAbsDiff {
+    type C = <(A, B) as PeanoAbsDiff>::C;
+}
+
+trait Range {
+    type Xs;
+}
+
+impl Range for Z {
+    type Xs = Nil;
+}
+
+impl<N> Range for S<N> where N: Range {
+    type Xs = Cons<N, N::Xs>;
+}
+
+fn accepts_true(_: True) {}
+fn legal_compare(x: <(S<Z>, S<Z>) as PeanoEqual>::T) {
+    accepts_true(x)
+}
+
+trait Apply {
+    type R;
+}
+
+struct Conj1<List>(PhantomData<List>);
+
+impl<List, X> Apply for (Conj1<List>, X) {
+    type R = Cons<X, List>;
+}
+
+trait Map {
+    type Ys;
+}
+
+impl<F> Map for (F, Nil) {
+    type Ys = Nil;
+}
+
+impl<F, X, Xs> Map for (F, Cons<X, Xs>) where (F, X): Apply, (F, Xs): Map {
+    type Ys = Cons<<(F, X) as Apply>::R, <(F, Xs) as Map>::Ys>;
+}
+
+trait MapCat {
+    type Zs;
+}
+
+impl<F> MapCat for (F, Nil) {
+    type Zs = Nil;
+}
+
+impl<F, Xs> 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;
+}
+
+impl<X, Ys> AppendIf for (True, X, Ys) {
+    type Zs = Cons<X, Ys>;
+}
+
+impl<X, Ys> AppendIf for (False, X, Ys) {
+    type Zs = Ys;
+}
+
+trait Filter {
+    type Ys;
+}
+
+impl<F> Filter for (F, Nil) {
+    type Ys = Nil;
+}
+
+impl<F, X, Xs> Filter for (F, Cons<X, Xs>) 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 Queen<X, Y>(PhantomData<X>, PhantomData<Y>);
+struct Queen1<X>(PhantomData<X>);
+
+impl<X, Y> Apply for (Queen1<X>, Y) {
+    type R = Queen<X, Y>;
+}
+
+trait QueensInRow {
+    type Queens;
+}
+
+impl<N, X> QueensInRow for (N, X) where N: Range, (Queen1<X>, <N as Range>::Xs): Map {
+    type Queens = <(Queen1<X>, <N as Range>::Xs) as Map>::Ys;
+}
+
+trait Threatens {
+    type T;
+}
+
+impl<Ax, Ay, Bx, By> 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>(PhantomData<A>);
+
+impl<A, B> Apply for (Threatens1<A>, B) where (A, B): Threatens {
+    type R = <(A, B) as Threatens>::T;
+}
+
+trait Safe {
+    type T;
+}
+
+impl<Config, Queen> Safe for (Config, Queen)
+    where (Threatens1<Queen>, Config): Map,
+          <(Threatens1<Queen>, Config) as Map>::Ys: AnyTrue,
+          <<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T: Not {
+    type T = <<<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T as Not>::B;
+}
+
+struct Safe1<Config>(PhantomData<Config>);
+
+impl<Config, Queen> Apply for (Safe1<Config>, Queen) where (Config, Queen): Safe {
+    type R = <(Config, Queen) as Safe>::T;
+}
+
+trait AddQueen {
+    type Cs;
+}
+
+impl<N, X, C> AddQueen for (N, X, C)
+    where (N, X): QueensInRow,
+          (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter,
+          <(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys: Map {
+    type Cs = <<(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys as Map>::Ys;
+}
+
+struct AddQueen2<N, X>(PhantomData<N>, PhantomData<X>);
+
+impl<N, X, C> Apply for (AddQueen2<N, X>, C) where (N, X, C): AddQueen {
+    type R = <(N, X, C) as AddQueen>::Cs;
+}
+
+trait AddQueenToAll {
+    type CsPrime;
+}
+
+impl<N, X, Cs> AddQueenToAll for (N, X, Cs) where (AddQueen2<N, X>, Cs): MapCat {
+    type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat>::Zs;
+}
+
+trait AddQueensIf {
+    type CsPrime;
+}
+
+impl<N, X, Cs> AddQueensIf for (False, N, X, Cs) {
+    type CsPrime = Cs;
+}
+
+impl<N, X, Cs> AddQueensIf for (True, N, X, Cs)
+    where (N, X, Cs): AddQueenToAll,
+          (N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime): AddQueens {
+    type CsPrime = <(N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
+}
+
+trait AddQueens {
+    type CsPrime;
+}
+
+impl<N, X, Cs> AddQueens for (N, X, Cs)
+    where (X, N): PeanoLT,
+          (<(X, N) as PeanoLT>::T, N, X, Cs): AddQueensIf {
+    type CsPrime = <(<(X, N) as PeanoLT>::T, N, X, Cs) as AddQueensIf>::CsPrime;
+}
+
+trait Solution {
+    type C;
+}
+
+impl<N> Solution for N where (N, Z, Cons<Nil, Nil>): AddQueens, <(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime: First {
+    type C = <<(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime as First>::X;
+}
+
+fn solve() -> <N6 as Solution>::C {
+    todo!()
+}
+
+fn main() {
+    // we should be able to read the type off the error here
+    let _: () = solve();
+}
-- 
cgit v1.2.3