diff options
| -rw-r--r-- | src/main.rs | 309 |
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 { |