aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main.rs309
1 files 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<X, XS>(PhantomData<X>, PhantomData<XS>);
-
-trait First {
- type X;
+trait Typed {
+ type Type;
}
-impl First for Nil {
- type X = Nil;
+struct ListType<T>(PhantomData<T>);
+
+struct Nil<T>(PhantomData<T>);
+impl<T> Typed for Nil<T> { type Type = ListType<T>; }
+struct Cons<X, XS>(PhantomData<X>, PhantomData<XS>);
+impl<T, X: Typed<Type=T>, XS: Typed<Type=ListType<T>>> Typed for Cons<X, XS> { type Type = ListType<T>; }
+
+trait First<T>: Typed<Type=ListType<T>> {
+ type X: Typed<Type=T>;
}
-impl<X, XS> First for Cons<X, XS> {
+impl<T, X: Typed<Type=T>, XS: Typed<Type=ListType<T>>> First<T> for Cons<X, XS> {
type X = X;
}
-trait ListConcat {
- type C;
+trait ListConcat<X> {
+ type C: Typed<Type=ListType<X>>;
}
-impl<X> ListConcat for (Nil, X) {
+impl<T, X: Typed<Type=ListType<T>>> ListConcat<T> for (Nil<T>, 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>;
+impl<T, A: Typed<Type=T>, As: Typed<Type=ListType<T>>, Bs: Typed<Type=ListType<T>>> ListConcat<T> for (Cons<A, As>, Bs)
+ where (As, Bs): ListConcat<T> {
+ type C = Cons<A, <(As, Bs) as ListConcat<T>>::C>;
}
-trait ListConcatAll {
- type L;
+trait ListConcatAll<T>: Typed<Type=ListType<ListType<T>>> {
+ type L: Typed<Type=ListType<T>>;
}
-impl ListConcatAll for Nil {
- type L = Nil;
+impl<T> ListConcatAll<T> for Nil<ListType<T>> {
+ type L = Nil<T>;
}
-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;
+impl<T, Chunk: Typed<Type=ListType<T>>, Rest: Typed<Type=ListType<ListType<T>>>> ListConcatAll<T> for Cons<Chunk, Rest>
+ where Rest: ListConcatAll<T>, (Chunk, <Rest as ListConcatAll<T>>::L): ListConcat<T> {
+ type L = <(Chunk, <Rest as ListConcatAll<T>>::L) as ListConcat<T>>::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=BoolType> {
+ type B: Typed<Type=BoolType>;
}
impl Not for True {
@@ -59,7 +69,7 @@ impl Not for False {
}
trait Or {
- type B;
+ type B: Typed<Type=BoolType>;
}
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=ListType<BoolType>> {
+ type T: Typed<Type=BoolType>;
}
-impl AnyTrue for Nil {
+impl AnyTrue for Nil<BoolType> {
type T = False;
}
-impl<More> AnyTrue for Cons<True, More> {
+impl<More: Typed<Type=ListType<BoolType>>> AnyTrue for Cons<True, More> {
type T = True;
}
@@ -94,174 +104,207 @@ 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>;
+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=NatType> {
+ type N: Typed<Type=NatType>;
+}
+
+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<Type=BoolType>;
}
-impl PeanoEqual for (Z, Z) {
+impl PeanoEqual for (N0, N0) {
type T = True;
}
-impl<A> PeanoEqual for (S<A>, Z) {
+impl<A, N: Succ<N=A>> PeanoEqual for (N, N0) {
type T = False;
}
-impl<B> PeanoEqual for (Z, S<B>) {
+impl<B, N: Succ<N=B>> PeanoEqual for (N0, N) {
type T = False;
}
-impl<A, B> PeanoEqual for (S<A>, S<B>) where (A, B): PeanoEqual {
+impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoEqual for (SA, SB) where (A, B): PeanoEqual {
type T = <(A, B) as PeanoEqual>::T;
}
trait PeanoLT {
- type T;
+ type T: Typed<Type=BoolType>;
}
-impl PeanoLT for (Z, Z) {
+impl PeanoLT for (N0, N0) {
type T = False;
}
-impl<X> PeanoLT for (S<X>, Z) {
+impl<X, SX: Succ<N=X>> PeanoLT for (SX, N0) {
type T = False;
}
-impl<X> PeanoLT for (Z, S<X>) {
+impl<X, SX: Succ<N=X>> PeanoLT for (N0, SX) {
type T = True;
}
-impl<A, B> PeanoLT for (S<A>, S<B>) where (A, B): PeanoLT {
+impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoLT for (SA, SB) where (A, B): PeanoLT {
type T = <(A, B) as PeanoLT>::T;
}
trait PeanoAbsDiff {
- type C;
+ type C: Typed<Type=NatType>;
}
-impl PeanoAbsDiff for (Z, Z) {
- type C = Z;
+impl PeanoAbsDiff for (N0, N0) {
+ type C = N0;
}
-impl<B> PeanoAbsDiff for (Z, S<B>) {
- type C = S<B>;
+impl<B, SB: Succ<N=B>> PeanoAbsDiff for (N0, SB) {
+ type C = SB;
}
-impl<A> PeanoAbsDiff for (S<A>, Z) {
- type C = S<A>;
+impl<A, SA: Succ<N=A>> PeanoAbsDiff for (SA, N0) {
+ type C = SA;
}
-impl<A, B> PeanoAbsDiff for (S<A>, S<B>) where (A, B): PeanoAbsDiff {
+impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoAbsDiff for (SA, SB) where (A, B): PeanoAbsDiff {
type C = <(A, B) as PeanoAbsDiff>::C;
}
-trait Range {
- type Xs;
+trait Range: Typed<Type=NatType> {
+ type Xs: Typed<Type=ListType<NatType>>;
}
-impl Range for Z {
- type Xs = Nil;
+impl Range for N0 {
+ type Xs = Nil<NatType>;
}
-impl<N> Range for S<N> where N: Range {
+impl<N, SN: Succ<N=N>> Range for SN where N: Range {
type Xs = Cons<N, N::Xs>;
}
fn accepts_true(_: True) {}
-fn legal_compare(x: <(S<Z>, S<Z>) as PeanoEqual>::T) {
+fn legal_compare(x: <(N1, N1) as PeanoEqual>::T) {
accepts_true(x)
}
-trait Apply {
- type R;
+struct Fn1Type<X, R>(PhantomData<X>, PhantomData<R>);
+
+trait Apply<T> {
+ type R: Typed<Type=T>;
}
-struct Conj1<List>(PhantomData<List>);
+struct Conj1<List: Typed<Type=ListType<T>>, T>(PhantomData<List>);
+impl<T, List: Typed<Type=ListType<T>>> Typed for Conj1<List, T> { type Type = Fn1Type<T, ListType<T>>; }
-impl<List, X> Apply for (Conj1<List>, X) {
+impl<T, List: Typed<Type=ListType<T>>, X: Typed<Type=T>> Apply<ListType<T>> for (Conj1<List, T>, X) {
type R = Cons<X, List>;
}
-trait Map {
- type Ys;
+trait Map<T> {
+ type Ys: Typed<Type=ListType<T>>;
}
-impl<F> Map for (F, Nil) {
- type Ys = Nil;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, T2>>> Map<T2> for (F, Nil<T1>) {
+ type Ys = Nil<T2>;
}
-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>;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, T2>>, X: Typed<Type=T1>, Xs: Typed<Type=ListType<T1>>> Map<T2> for (F, Cons<X, Xs>)
+ where (F, X): Apply<T2>, (F, Xs): Map<T2> {
+ type Ys = Cons<<(F, X) as Apply<T2>>::R, <(F, Xs) as Map<T2>>::Ys>;
}
-trait MapCat {
- type Zs;
+trait MapCat<T> {
+ type Zs: Typed<Type=ListType<T>>;
}
-impl<F> MapCat for (F, Nil) {
- type Zs = Nil;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, ListType<T2>>>> MapCat<T2> for (F, Nil<T1>) {
+ type Zs = Nil<T2>;
}
-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;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, ListType<T2>>>, Xs: Typed<Type=ListType<T1>>> MapCat<T2> for (F, Xs)
+ where (F, Xs): Map<ListType<T2>>, <(F, Xs) as Map<ListType<T2>>>::Ys: ListConcatAll<T2> {
+ type Zs = <<(F, Xs) as Map<ListType<T2>>>::Ys as ListConcatAll<T2>>::L;
}
-trait AppendIf {
- type Zs;
+trait AppendIf<T> {
+ type Zs: Typed<Type=ListType<T>>;
}
-impl<X, Ys> AppendIf for (True, X, Ys) {
+impl<T, X: Typed<Type=T>, Ys: Typed<Type=ListType<T>>> AppendIf<T> for (True, X, Ys) {
type Zs = Cons<X, Ys>;
}
-impl<X, Ys> AppendIf for (False, X, Ys) {
+impl<T, X: Typed<Type=T>, Ys: Typed<Type=ListType<T>>> AppendIf<T> for (False, X, Ys) {
type Zs = Ys;
}
-trait Filter {
- type Ys;
+trait Filter<T> {
+ type Ys: Typed<Type=ListType<T>>;
}
-impl<F> Filter for (F, Nil) {
- type Ys = Nil;
+impl<T, F: Typed<Type=Fn1Type<T, BoolType>>> Filter<T> for (F, Nil<T>) {
+ type Ys = Nil<T>;
}
-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;
+impl<T, F: Typed<Type=Fn1Type<T, BoolType>>, X: Typed<Type=T>, Xs: Typed<Type=ListType<T>>> Filter<T> for (F, Cons<X, Xs>)
+ where (F, X): Apply<BoolType>, (F, Xs): Filter<T>,
+ (<(F, X) as Apply<BoolType>>::R, X, <(F, Xs) as Filter<T>>::Ys): AppendIf<T> {
+ type Ys = <(<(F, X) as Apply<BoolType>>::R, X, <(F, Xs) as Filter<T>>::Ys) as AppendIf<T>>::Zs;
}
-struct Queen<X, Y>(PhantomData<X>, PhantomData<Y>);
-struct Queen1<X>(PhantomData<X>);
+struct QueenType;
+
+struct Queen<X: Typed<Type=NatType>, Y: Typed<Type=NatType>>(PhantomData<X>, PhantomData<Y>);
+impl<X, Y> Typed for Queen<X, Y> { type Type = QueenType; }
+struct Queen1<X: Typed<Type=NatType>>(PhantomData<X>);
+impl<X> Typed for Queen1<X> { type Type = Fn1Type<NatType, QueenType>; }
-impl<X, Y> Apply for (Queen1<X>, Y) {
+impl<X: Typed<Type=NatType>, Y: Typed<Type=NatType>> Apply<QueenType> for (Queen1<X>, Y) {
type R = Queen<X, Y>;
}
trait QueensInRow {
- type Queens;
+ type Queens: Typed<Type=ListType<QueenType>>;
}
-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;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>> QueensInRow for (N, X)
+ where N: Range, (Queen1<X>, <N as Range>::Xs): Map<QueenType> {
+ type Queens = <(Queen1<X>, <N as Range>::Xs) as Map<QueenType>>::Ys;
}
trait Threatens {
- type T;
+ type T: Typed<Type=BoolType>;
}
-impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
+impl<Ax: Typed<Type=NatType>, Ay: Typed<Type=NatType>, Bx: Typed<Type=NatType>, By: Typed<Type=NatType>> 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,
@@ -274,84 +317,90 @@ impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
) as Or>::B;
}
-struct Threatens1<A>(PhantomData<A>);
+struct Threatens1<A: Typed<Type=QueenType>>(PhantomData<A>);
+impl<A> Typed for Threatens1<A> { type Type = Fn1Type<QueenType, BoolType>; }
-impl<A, B> Apply for (Threatens1<A>, B) where (A, B): Threatens {
+impl<A: Typed<Type=QueenType>, B: Typed<Type=QueenType>> Apply<BoolType> for (Threatens1<A>, B)
+ where (A, B): Threatens {
type R = <(A, B) as Threatens>::T;
}
trait Safe {
- type T;
+ type T: Typed<Type=BoolType>;
}
-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;
+impl<Config: Typed<Type=ListType<QueenType>>, Queen: Typed<Type=QueenType>> Safe for (Config, Queen)
+ where (Threatens1<Queen>, Config): Map<BoolType>,
+ <(Threatens1<Queen>, Config) as Map<BoolType>>::Ys: AnyTrue,
+ <<(Threatens1<Queen>, Config) as Map<BoolType>>::Ys as AnyTrue>::T: Not {
+ type T = <<<(Threatens1<Queen>, Config) as Map<BoolType>>::Ys as AnyTrue>::T as Not>::B;
}
-struct Safe1<Config>(PhantomData<Config>);
+struct Safe1<Config: Typed<Type=ListType<QueenType>>>(PhantomData<Config>);
-impl<Config, Queen> Apply for (Safe1<Config>, Queen) where (Config, Queen): Safe {
+impl<Config: Typed<Type=ListType<QueenType>>, Queen> Apply<BoolType> for (Safe1<Config>, Queen)
+ where (Config, Queen): Safe {
type R = <(Config, Queen) as Safe>::T;
}
trait AddQueen {
- type Cs;
+ type Cs: Typed<Type=ListType<QueenType>>;
}
-impl<N, X, C> AddQueen for (N, X, C)
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, C: Typed<Type=ListType<QueenType>>> 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;
+ (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter<QueenType>,
+ <(Conj1<C, QueenType>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter<QueenType>>::Ys: Map<QueenType> {
+ type Cs = <<(Conj1<C, QueenType>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter<QueenType>>::Ys as Map<QueenType>>::Ys;
}
-struct AddQueen2<N, X>(PhantomData<N>, PhantomData<X>);
+struct AddQueen2<N: Typed<Type=NatType>, X: Typed<Type=NatType>>(PhantomData<N>, PhantomData<X>);
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>> Typed for AddQueen2<N, X> { type Type = Fn1Type<ListType<QueenType>, ListType<QueenType>>; }
-impl<N, X, C> Apply for (AddQueen2<N, X>, C) where (N, X, C): AddQueen {
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, C: Typed<Type=ListType<QueenType>>> Apply<ListType<QueenType>> for (AddQueen2<N, X>, C)
+ where (N, X, C): AddQueen {
type R = <(N, X, C) as AddQueen>::Cs;
}
trait AddQueenToAll {
- type CsPrime;
+ type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
}
-impl<N, X, Cs> AddQueenToAll for (N, X, Cs) where (AddQueen2<N, X>, Cs): MapCat {
- type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat>::Zs;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueenToAll for (N, X, Cs)
+ where (AddQueen2<N, X>, Cs): MapCat<ListType<QueenType>> {
+ type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat<ListType<QueenType>>>::Zs;
}
trait AddQueensIf {
- type CsPrime;
+ type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
}
-impl<N, X, Cs> AddQueensIf for (False, N, X, Cs) {
+impl<N: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueensIf for (N, N0, 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;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>, SX: Succ<N=X>> 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<Type=ListType<ListType<QueenType>>>;
}
-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;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> 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<Type=ListType<QueenType>>;
}
-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;
+impl<N: Typed<Type=NatType>> Solution for N
+ where (N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>): AddQueens, <(N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>) as AddQueens>::CsPrime: First<ListType<QueenType>> {
+ type C = <<(N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>) as AddQueens>::CsPrime as First<ListType<QueenType>>>::X;
}
fn solve() -> <N6 as Solution>::C {
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 13:20:07 +0000