From 23a0b3aa35eff1056ad3b160aaadaee5bb9c4a07 Mon Sep 17 00:00:00 2001
From: Melody Horn
Date: Sat, 13 Mar 2021 11:37:27 0700
Subject: add types to this typelevel programming clusterfuck
also make the numbers count down instead of up in AddQueens, which changes where the infinite recursion lives but doesn't fix it

src/main.rs  309 +++++++++++++++++++++++++++++++++++
1 file changed, 179 insertions(+), 130 deletions()
diff git a/src/main.rs b/src/main.rs
index 7612805..2de2e3a 100644
 a/src/main.rs
+++ b/src/main.rs
@@ 4,50 +4,60 @@
//! [source 2](https://sdleffler.github.io/RustTypeSystemTuringComplete/)
use std::marker::PhantomData;
struct Nil;
struct Cons(PhantomData, PhantomData);

trait First {
 type X;
+trait Typed {
+ type Type;
}
impl First for Nil {
 type X = Nil;
+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 First for Cons {
+impl, XS: Typed>> First for Cons {
type X = X;
}
trait ListConcat {
 type C;
+trait ListConcat {
+ type C: Typed>;
}
impl ListConcat for (Nil, X) {
+impl>> ListConcat for (Nil, X) {
type C = X;
}
impl ListConcat for (Cons, Bs) where (As, Bs): ListConcat {
 type C = Cons::C>;
+impl, As: Typed>, Bs: Typed>> ListConcat for (Cons, Bs)
+ where (As, Bs): ListConcat {
+ type C = Cons>::C>;
}
trait ListConcatAll {
 type L;
+trait ListConcatAll: Typed>> {
+ type L: Typed>;
}
impl ListConcatAll for Nil {
 type L = Nil;
+impl ListConcatAll for Nil> {
+ type L = Nil;
}
impl ListConcatAll for Cons where Rest: ListConcatAll, (Chunk, ::L): ListConcat {
 type L = <(Chunk, ::L) as ListConcat>::C;
+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 {
 type B;
+trait Not: Typed {
+ type B: Typed;
}
impl Not for True {
@@ 59,7 +69,7 @@ impl Not for False {
}
trait Or {
 type B;
+ type B: Typed;
}
impl Or for (True, True) {
@@ 78,15 +88,15 @@ impl Or for (False, False) {
type B = False;
}
trait AnyTrue {
 type T;
+trait AnyTrue: Typed> {
+ type T: Typed;
}
impl AnyTrue for Nil {
+impl AnyTrue for Nil {
type T = False;
}
impl AnyTrue for Cons {
+impl>> AnyTrue for Cons {
type T = True;
}
@@ 94,174 +104,207 @@ impl AnyTrue for Cons where List: AnyTrue {
type T = ::T;
}
struct Z;
struct S(PhantomData);

type N0 = Z;
type N1 = S;
type N2 = S;
type N3 = S;
type N4 = S;
type N5 = S;
type N6 = S;
type N7 = S;
type N8 = S;
+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;
+ type T: Typed;
}
impl PeanoEqual for (Z, Z) {
+impl PeanoEqual for (N0, N0) {
type T = True;
}
impl PeanoEqual for (S, Z) {
+impl> PeanoEqual for (N, N0) {
type T = False;
}
impl PeanoEqual for (Z, S) {
+impl> PeanoEqual for (N0, N) {
type T = False;
}
impl PeanoEqual for (S
, S) where (A, B): PeanoEqual {
+impl, SB: Succ> PeanoEqual for (SA, SB) where (A, B): PeanoEqual {
type T = <(A, B) as PeanoEqual>::T;
}
trait PeanoLT {
 type T;
+ type T: Typed;
}
impl PeanoLT for (Z, Z) {
+impl PeanoLT for (N0, N0) {
type T = False;
}
impl PeanoLT for (S, Z) {
+impl> PeanoLT for (SX, N0) {
type T = False;
}
impl PeanoLT for (Z, S) {
+impl> PeanoLT for (N0, SX) {
type T = True;
}
impl PeanoLT for (S, S) where (A, B): PeanoLT {
+impl, SB: Succ> PeanoLT for (SA, SB) where (A, B): PeanoLT {
type T = <(A, B) as PeanoLT>::T;
}
trait PeanoAbsDiff {
 type C;
+ type C: Typed;
}
impl PeanoAbsDiff for (Z, Z) {
 type C = Z;
+impl PeanoAbsDiff for (N0, N0) {
+ type C = N0;
}
impl PeanoAbsDiff for (Z, S) {
 type C = S;
+impl> PeanoAbsDiff for (N0, SB) {
+ type C = SB;
}
impl PeanoAbsDiff for (S, Z) {
 type C = S;
+impl> PeanoAbsDiff for (SA, N0) {
+ type C = SA;
}
impl PeanoAbsDiff for (S, S) where (A, B): PeanoAbsDiff {
+impl, SB: Succ> PeanoAbsDiff for (SA, SB) where (A, B): PeanoAbsDiff {
type C = <(A, B) as PeanoAbsDiff>::C;
}
trait Range {
 type Xs;
+trait Range: Typed {
+ type Xs: Typed>;
}
impl Range for Z {
 type Xs = Nil;
+impl Range for N0 {
+ type Xs = Nil;
}
impl Range for S where N: Range {
+impl> Range for SN where N: Range {
type Xs = Cons;
}
fn accepts_true(_: True) {}
fn legal_compare(x: <(S, S) as PeanoEqual>::T) {
+fn legal_compare(x: <(N1, N1) as PeanoEqual>::T) {
accepts_true(x)
}
trait Apply {
 type R;
+struct Fn1Type(PhantomData, PhantomData);
+
+trait Apply {
+ type R: Typed;
}
struct Conj1(PhantomData);
+struct Conj1>, T>(PhantomData);
+impl>> Typed for Conj1 { type Type = Fn1Type>; }
impl Apply for (Conj1, X) {
+impl>, X: Typed> Apply> for (Conj1, X) {
type R = Cons;
}
trait Map {
 type Ys;
+trait Map {
+ type Ys: Typed>;
}
impl Map for (F, Nil) {
 type Ys = Nil;
+impl>> Map for (F, Nil) {
+ type Ys = Nil;
}
impl Map for (F, Cons) where (F, X): Apply, (F, Xs): Map {
 type Ys = Cons<<(F, X) as Apply>::R, <(F, Xs) as Map>::Ys>;
+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;
+trait MapCat {
+ type Zs: Typed>;
}
impl MapCat for (F, Nil) {
 type Zs = Nil;
+impl>>> MapCat for (F, Nil) {
+ type Zs = Nil;
}
impl MapCat for (F, Xs) where (F, Xs): Map, <(F, Xs) as Map>::Ys: ListConcatAll {
 type Zs = <<(F, Xs) as Map>::Ys as ListConcatAll>::L;
+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;
+trait AppendIf {
+ type Zs: Typed>;
}
impl AppendIf for (True, X, Ys) {
+impl, Ys: Typed>> AppendIf for (True, X, Ys) {
type Zs = Cons;
}
impl AppendIf for (False, X, Ys) {
+impl, Ys: Typed>> AppendIf for (False, X, Ys) {
type Zs = Ys;
}
trait Filter {
 type Ys;
+trait Filter {
+ type Ys: Typed>;
}
impl Filter for (F, Nil) {
 type Ys = Nil;
+impl>> Filter for (F, Nil) {
+ type Ys = Nil;
}
impl 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;
+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 Queen(PhantomData, PhantomData);
struct Queen1(PhantomData);
+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 Apply for (Queen1, Y) {
+impl, Y: Typed> Apply for (Queen1, Y) {
type R = Queen;
}
trait QueensInRow {
 type Queens;
+ type Queens: Typed>;
}
impl QueensInRow for (N, X) where N: Range, (Queen1, ::Xs): Map {
 type Queens = <(Queen1, ::Xs) as Map>::Ys;
+impl, X: Typed> QueensInRow for (N, X)
+ where N: Range, (Queen1, ::Xs): Map {
+ type Queens = <(Queen1, ::Xs) as Map>::Ys;
}
trait Threatens {
 type T;
+ type T: Typed;
}
impl Threatens for (Queen, Queen)
+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,
@@ 274,84 +317,90 @@ impl Threatens for (Queen, Queen)
) as Or>::B;
}
struct Threatens1
(PhantomData);
+struct Threatens1>(PhantomData);
+impl Typed for Threatens1 { type Type = Fn1Type; }
impl Apply for (Threatens1, B) where (A, B): Threatens {
+impl, B: Typed> Apply for (Threatens1, B)
+ where (A, B): Threatens {
type R = <(A, B) as Threatens>::T;
}
trait Safe {
 type T;
+ type T: Typed;
}
impl 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;
+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);
+struct Safe1>>(PhantomData);
impl Apply for (Safe1, Queen) where (Config, Queen): Safe {
+impl>, Queen> Apply for (Safe1, Queen)
+ where (Config, Queen): Safe {
type R = <(Config, Queen) as Safe>::T;
}
trait AddQueen {
 type Cs;
+ type Cs: Typed>;
}
impl AddQueen for (N, X, C)
+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;
+ (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(PhantomData, PhantomData);
+struct AddQueen2, X: Typed>(PhantomData, PhantomData);
+impl, X: Typed> Typed for AddQueen2 { type Type = Fn1Type, ListType>; }
impl Apply for (AddQueen2, C) where (N, X, C): AddQueen {
+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;
+ type CsPrime: Typed>>;
}
impl AddQueenToAll for (N, X, Cs) where (AddQueen2, Cs): MapCat {
 type CsPrime = <(AddQueen2, Cs) as MapCat>::Zs;
+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;
+ type CsPrime: Typed>>;
}
impl AddQueensIf for (False, N, X, Cs) {
+impl, Cs: Typed>>> AddQueensIf for (N, N0, Cs) {
type CsPrime = Cs;
}
impl AddQueensIf for (True, N, X, Cs)
 where (N, X, Cs): AddQueenToAll,
 (N, S, <(N, X, Cs) as AddQueenToAll>::CsPrime): AddQueens {
 type CsPrime = <(N, S, <(N, X, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
+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;
+ type CsPrime: Typed>>;
}
impl 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;
+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;
+ type C: Typed>;
}
impl Solution for N where (N, Z, Cons): AddQueens, <(N, Z, Cons) as AddQueens>::CsPrime: First {
 type C = <<(N, Z, Cons) as AddQueens>::CsPrime as First>::X;
+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 {

cgit v1.2.1