diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main.chalk | 336 | ||||
| -rw-r--r-- | src/main.rs | 364 |
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(); +} |