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 type-level 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(-) (limited to 'src') 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.3