aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMelody Horn <melody@boringcactus.com>2021-03-12 18:55:07 -0700
committerMelody Horn <melody@boringcactus.com>2021-03-12 18:55:07 -0700
commita07fed3794c0f91b4c2c7cd2332163b8cf031a72 (patch)
tree5386439f72b993421ba7e2dcb8cb84e1a748373c /src
downloadrust-typing-the-technical-interview-a07fed3794c0f91b4c2c7cd2332163b8cf031a72.tar.gz
rust-typing-the-technical-interview-a07fed3794c0f91b4c2c7cd2332163b8cf031a72.zip
a first attempt at heresy
Diffstat (limited to 'src')
-rw-r--r--src/main.chalk336
-rw-r--r--src/main.rs364
2 files changed, 700 insertions, 0 deletions
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();
+}