BrainF*** in the Swift type system

Swift's type system is Turing-complete. The result was known (not to me when I went down this rabbit hole; I did this all on the speculation that Swift's type system is Turing complete), but I've not seen anyone prove it. So, let's reduce the Swift type system to a simple, but well-known-to-be-Turing-complete, language: BrainF***. (I'm not gonna censor that further. It's the name of the language, and not, in this context, a profanity. If you don't want to see it, don't read on.)

If you want to follow what I did, make sure you're familiar with BrainFuck (follow that wikipedia link, for example).

Implementing BrainFuck in the Swift type system

First we need numbers. The Peano axioms give us a convenient definition of natural numbers.

A natural number

protocol Nat {}

is either zero:

struct Zero: Nat {}

or it's the successor to another natural number:

struct Succ<Pred: Nat>: Nat {}

That's all that's needed (though it is a very Succy way to represent numbers).

typealias Three = Succ<Succ<Succ<Zero>>>

Since these are types, we can create a static property to provide the Int value of the type, for convenience:

protocol Nat {
    static var value: Int { get }
}
struct Zero: Nat {
    static var value: Int {
        0
    }
}
struct Succ<Pred: Nat>: Nat {
    static var value: Int {
        1 + Pred.value
    }
}

print(Succ<Succ<Succ<Zero>>>.value) // 3

Now, we want our BrainFuck program to be able to output something, to prove that it ran. So we need a representation of strings in the type system. We can do something similar to the natural numbers:

protocol Str {
    static var value: String { get }
    init()
}
struct EmptyStr: Str {
    init() {}
    static var value: String {
        ""
    }
}
struct Char<Unicode: Nat, Prefix: Str>: Str {
    init() {}
    static var value: String {
        var result = Prefix.value
        result.append(Character(UnicodeScalar(Unicode.value)!))
        return result
    }
}

Notice how Char forms a kind of "linked list" in the type system (Haskell calls this an HList).

Compile time strings in action:

typealias A = Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
typealias H = Succ<Succ<Succ<Succ<Succ<Succ<Succ<A>>>>>>>
typealias I = Succ<H>

print(Char<I, Char<H, EmptyStr>>.value) // HI

(very Succy)

We can use the same linked list trick to represent the two tapes in BrainFuck (data and instructions), using one list to represent the tape before the "head" of the machine, and another list to represent the tape after the "head".

Instructions can just be empty structs.

And then you can basically define the BrainFuck VM as a Swift type:

struct Machine<
    TapeLeft: MemoryTape,
    TapeCurrent: Nat,
    TapeRight: MemoryTape,
    ProgramLeft: ProgramTape,
    ProgramCurrent: Instr,
    ProgramRight: ProgramTape,
    Stack: StateStack,
    Output: Str
> { ... }

extension Machine where ProgramCurrent == Exited {
    var output: Output {
        .init()
    }
}

But then, how can we represent a state transition of this machine? Well, we can do that with a member function, which allows us to introduce generics:

    // increment as nonfinal instruction
    func step<OutputString, StateTail, NextInstr, Rest>() -> 
        // the result of calling this overload of step(): a
        // machine in the same state, except the value of
        // the current cell has been incremented 
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >
    where
        // conditions to call this overload of step: this
        // machine must be in the right state:
        //    * stepping through instructions
        //      (loops change this)
        Stack == Pushed<Step, StateTail>,
        //    * having at least one instruction remaining on
        //      the instruction tape
        ProgramRight == Instruction<NextInstr, Rest>,
        //    * currently executing an increment instruction
        ProgramCurrent == Inc
    {
        .init()
    }

If you did that 27 times for all the different states of the BrainFuck VM, you can get the result like this:

typealias MyMachine = Machine<...>

protocol Infer {
    associatedtype InferredType
    static var inferFrom: InferredType { get }
}
struct MyMachineOutput: Infer {
    static let inferFrom = MyMachine().step().step().step()....output
}
print(MyMachineOutput.InferredType.self) // something hideous
print(MyMachineOutput.InferredType.value) // the output of your program

The problem is, you need to know how many steps the machine will take to run and write the exact right number of calls to step(). Not only is that awful, it kinda feels like "doing the hard bit by hand" still. Feels like a dead-end...

A detour: @dynamicMemberLookup

Swift has a fun feature for adding "virtual" properties to types: KeyPath dynamic member lookup. Basically, you mark up your type with @dynamicMemberLookup, and provide a subscript with a particular signature, which accepts a KeyPath in some other type:

struct A {
    var s: String
}

@dynamicMemberLookup
struct ContainsA {
    var a: A
    subscript<R>(dynamicMember keyPath: KeyPath<A, R>) -> R {
        a[keyPath: keyPath]
    }
}

let ca = ContainsA(a: A(s: "hi"))
print(ca.s) // "hi"

And voilá, now your type magically has properties whose names are defined by some other type.

How does this help? Well, the lookup process for dynamic members is recursive. That is, when resolving the type of the argument to the subscript, dynamic member lookup may do more dynamic member lookup, invoking the same, or another, dynamicMember subscript on the same, or another, type...

So if we rewrite our step functions as dynamicMember subscripts:

    // increment as nonfinal instruction
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Inc
    {
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

where the root of the keyPath argument is the "next state", and the output of the dynamicMember subscript is the output type of the keypath in the "next state"... then the output type can actually be the output type of the whole execution of the machine. And now we can get the output like this:

struct MyMachineOutput: Infer {
    static let inferFrom = MyMachine().output
}
print(MyMachineOutput.InferredType.self) // something hideous
print(MyMachineOutput.InferredType.value) // the output of your program

OK, Let's do it! Let's write a BrainFuck program in the Swift type system! There's a fairly canonical "Hello, world!" program, you can find on the Wikipedia page. Let's do that, it's traditional:

// ++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-.<.+++.------.--------.>>+.>++.
typealias PrintHelloWorld = Machine<
    ToInfinityAndBeyond,
    Zero,
    ToInfinityAndBeyond,
    End,
    Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        End>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
    Pushed<Step, EmptyStack>,
    EmptyStr
>

struct PrintHelloWorldOutput: Infer {
    static let inferFrom = PrintHelloWorld().output
}

print(PrintHelloWorldOutput.InferredType.self)
print(PrintHelloWorldOutput.InferredType.value)

Go go gadget Xcode!

:stop_sign: The compiler is unable to type-check this expression in reasonable time; try breaking up the expression into distinct sub-expressions

Oh. Oh no. All this, for nothing?! :sob:

Well, let's do some spelunking in the compiler to find some esoteric command-line flags and give it all the time in the world to do the typechecking!

-Xfrontend -solver-memory-threshold -Xfrontend 4294967295 -Xfrontend -solver-expression-time-threshold=20000

And try again!

:stop_sign: The compiler is unable to type-check this expression in reasonable time; try breaking up the expression into distinct sub-expressions

Well, that's it. We can't print "Hello, world!" because the compiler needs more than 4GB of RAM to evaluate it. What else could we do, that's simpler? Lowercase ASCII has higher values than uppercase, maybe shouting will help?

// +++[->+++<]>[->++++>++++++++>+++++++++<<<]>>.+.<----.>>++.++++.<.---.>---.

typealias PrintHi = Machine<
    ToInfinityAndBeyond,
    Zero,
    ToInfinityAndBeyond,
    End,
    Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<LoopStart,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        End>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
Pushed<Step, EmptyStack>,
EmptyStr
>

struct PrintHiOutput: Infer {
    static let inferFrom = PrintHi().output
}

print(PrintHiOutput.InferredType.self)
print(PrintHiOutput.InferredType.value)

:arrow_right: Compiling main.swift (56s)

:white_check_mark: Build Succeeded

Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, Char<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, EmptyStr>>>>>>>>
HI SWIFT
55 Likes

Apologies to @Slava_Pestov who seems to care about the type system being sane, and @Douglas_Gregor and @xedin whose dynamic member lookup keypaths allowed me to close the loop on this idea.

Here's the full code, including ~800 lines of state transitions for the BrainFuck VM :sob: . Remember, you need those compiler flags from up above, or this will just time out!

protocol Nat {
    static var value: Int { get }
}
struct Zero: Nat {
    static var value: Int {
        0
    }
}
struct Succ<Pred: Nat>: Nat {
    static var value: Int {
        1 + Pred.value
    }
}

/*
print(Succ<Succ<Succ<Zero>>>.value)
*/

// ----

protocol Str {
    static var value: String { get }
    init()
}
struct EmptyStr: Str {
    init() {}
    static var value: String {
        ""
    }
}
struct Char<Unicode: Nat, Prefix: Str>: Str {
    init() {}
    static var value: String {
        var result = Prefix.value
        result.append(Character(UnicodeScalar(Unicode.value)!))
        return result
    }
}

/*
typealias A = Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
typealias H = Succ<Succ<Succ<Succ<Succ<Succ<Succ<A>>>>>>>
typealias I = Succ<H>

print(Char<I, Char<H, EmptyStr>>.value)
*/

// ----

protocol MemoryTape {}
struct ToInfinityAndBeyond: MemoryTape {}
struct Square<Value: Nat, Tail: MemoryTape>: MemoryTape {
    var value: Value
    var tail: Tail
}

// ----

protocol Instr {}
protocol SimpleInstr: Instr {}
struct Exited: Instr {}
struct Inc: SimpleInstr {}
struct Dec: SimpleInstr {}
struct Next: SimpleInstr {}
struct Prev: SimpleInstr {}
struct CharOut: SimpleInstr {}
struct LoopStart: Instr {}
struct LoopEnd: Instr {}

// ----

protocol ProgramTape {}
struct End: ProgramTape {}
struct Instruction<I: Instr, Rest: ProgramTape>: ProgramTape {
    var instruction: I
    var rest: ProgramTape
}

// ----

protocol MachineState {}
struct Step: MachineState {}
struct ScanForward: MachineState {}
struct ScanBackward: MachineState {}

protocol StateStack {}
struct EmptyStack: StateStack {}
struct Pushed<State: MachineState, Rest: StateStack>: StateStack {}

@dynamicMemberLookup
struct Machine<
    TapeLeft: MemoryTape,
    TapeCurrent: Nat,
    TapeRight: MemoryTape,
    ProgramLeft: ProgramTape,
    ProgramCurrent: Instr,
    ProgramRight: ProgramTape,
    Stack: StateStack,
    Output: Str
> {

    // increment as final instruction
    subscript<OutputString, StateTail>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == End,
        ProgramCurrent == Inc
    {
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // increment as nonfinal instruction
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Inc
    {
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // decrement as final instruction
    subscript<OutputString, StateTail, Pred>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Pred,
            TapeRight,
            Instruction<Dec, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramRight == End,
        ProgramCurrent == Dec
    {
        Machine<
            TapeLeft,
            Pred,
            TapeRight,
            Instruction<Dec, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // decrement as nonfinal instruction
    subscript<OutputString, StateTail, Pred, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Pred,
            TapeRight,
            Instruction<Dec, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Dec
    {
        Machine<
            TapeLeft,
            Pred,
            TapeRight,
            Instruction<Dec, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // next as final instruction, existing tape
    subscript<OutputString, StateTail, TapeRightFirst, TapeRightRest>(dynamicMember keyPath: KeyPath<
        Machine<
            Square<TapeCurrent, TapeLeft>,
            TapeRightFirst,
            TapeRightRest,
            Instruction<Next, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeRight == Square<TapeRightFirst, TapeRightRest>,
        ProgramRight == End,
        ProgramCurrent == Next
    {
        Machine<
            Square<TapeCurrent, TapeLeft>,
            TapeRightFirst,
            TapeRightRest,
            Instruction<Next, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // next as nonfinal instruction, existing tape
    subscript<OutputString, StateTail, TapeRightFirst, TapeRightRest, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            Square<TapeCurrent, TapeLeft>,
            TapeRightFirst,
            TapeRightRest,
            Instruction<Next, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeRight == Square<TapeRightFirst, TapeRightRest>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Next
    {
        Machine<
            Square<TapeCurrent, TapeLeft>,
            TapeRightFirst,
            TapeRightRest,
            Instruction<Next, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // next as final instruction, creating tape
    subscript<OutputString, StateTail>(dynamicMember keyPath: KeyPath<
        Machine<
            Square<TapeCurrent, TapeLeft>,
            Zero,
            ToInfinityAndBeyond,
            Instruction<Next, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeRight == ToInfinityAndBeyond,
        ProgramRight == End,
        ProgramCurrent == Next
    {
        Machine<
            Square<TapeCurrent, TapeLeft>,
            Zero,
            ToInfinityAndBeyond,
            Instruction<Next, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // next as nonfinal instruction, creating tape
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            Square<TapeCurrent, TapeLeft>,
            Zero,
            ToInfinityAndBeyond,
            Instruction<Next, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeRight == ToInfinityAndBeyond,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Next
    {
        Machine<
            Square<TapeCurrent, TapeLeft>,
            Zero,
            ToInfinityAndBeyond,
            Instruction<Next, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // prev as final instruction, existing tape
    subscript<OutputString, StateTail, TapeLeftFirst, TapeLeftRest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeftRest,
            TapeLeftFirst,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeLeft == Square<TapeLeftFirst, TapeLeftRest>,
        ProgramRight == End,
        ProgramCurrent == Prev
    {
        Machine<
            TapeLeftRest,
            TapeLeftFirst,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // prev as nonfinal instruction, existing tape
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            ToInfinityAndBeyond,
            Zero,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeLeft == ToInfinityAndBeyond,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Prev
    {
        Machine<
            ToInfinityAndBeyond,
            Zero,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // prev as final instruction, creating tape
    subscript<OutputString, StateTail>(dynamicMember keyPath: KeyPath<
        Machine<
            ToInfinityAndBeyond,
            Zero,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeLeft == ToInfinityAndBeyond,
        ProgramRight == End,
        ProgramCurrent == Prev
    {
        Machine<
            ToInfinityAndBeyond,
            Zero,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // prev as nonfinal instruction, creating tape
    subscript<OutputString, StateTail, TapeLeftFirst, TapeLeftRest, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeftRest,
            TapeLeftFirst,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeLeft == Square<TapeLeftFirst, TapeLeftRest>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Prev
    {
        Machine<
            TapeLeftRest,
            TapeLeftFirst,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // charout as final instruction
    subscript<OutputString, StateTail>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<CharOut, ProgramLeft>,
            Exited,
            End,
            Stack,
            Char<TapeCurrent, Output>
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == End,
        ProgramCurrent == CharOut
    {
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<CharOut, ProgramLeft>,
            Exited,
            End,
            Stack,
            Char<TapeCurrent, Output>
        >()[keyPath: keyPath]
    }

    // charout as nonfinal instruction
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<CharOut, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Char<TapeCurrent, Output>
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == CharOut
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<CharOut, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Char<TapeCurrent, Output>
        >()[keyPath: keyPath]
    }

    // loopstart, nonzero, nonfinal
    subscript<OutputString, StateTail, Pred, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramCurrent == LoopStart,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // loopstart, zero, nonfinal
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<ScanForward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Zero,
        ProgramCurrent == LoopStart,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<ScanForward, Stack>,
            Output
        >()[keyPath: keyPath]
    }

    // loopend, zero, final
    subscript<OutputString, StateTail>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Zero,
        ProgramCurrent == LoopEnd,
        ProgramRight == End
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            Exited,
            End,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // loopend, zero, nonfinal
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Zero,
        ProgramCurrent == LoopEnd,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // loopend, nonzero, noninitial
    subscript<OutputString, StateTail, Pred, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopEnd, ProgramRight>,
            Pushed<ScanBackward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramLeft == Instruction<PrevInstr, Rest>,
        ProgramCurrent == LoopEnd
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopEnd, ProgramRight>,
            Pushed<ScanBackward, Stack>,
            Output
        >()[keyPath: keyPath]
    }

    // scan forward over simple instruction
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<ProgramCurrent, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramCurrent: SimpleInstr,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<ProgramCurrent, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // scan forward over loopstart
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<ScanForward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == LoopStart
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<ScanForward, Stack>,
            Output
        >()[keyPath: keyPath]
    }

    // scan forward over loopend, final
    subscript<OutputString, StateTail>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            Exited,
            End,
            StateTail,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramRight == End,
        ProgramCurrent == LoopEnd
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            Exited,
            End,
            StateTail,
            Output
        >()[keyPath: keyPath]
    }

    // scan forward over loopend, nonfinal
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            NextInstr,
            Rest,
            StateTail,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == LoopEnd
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            NextInstr,
            Rest,
            StateTail,
            Output
        >()[keyPath: keyPath]
    }

    // scan backward over simple instruction
    subscript<OutputString, StateTail, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<ProgramCurrent, ProgramRight>,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, StateTail>,
        ProgramCurrent: SimpleInstr,
        ProgramLeft == Instruction<PrevInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<ProgramCurrent, ProgramRight>,
            Stack,
            Output
        >()[keyPath: keyPath]
    }

    // scan backward over loopend
    subscript<OutputString, StateTail, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopEnd, ProgramRight>,
            Pushed<ScanBackward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, StateTail>,
        ProgramCurrent == LoopEnd,
        ProgramLeft == Instruction<PrevInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopEnd, ProgramRight>,
            Pushed<ScanBackward, Stack>,
            Output
        >()[keyPath: keyPath]
    }

    // scan backward over loopstart, nested
    subscript<OutputString, StateTail, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopStart, ProgramRight>,
            Pushed<ScanBackward, StateTail>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, Pushed<ScanBackward, StateTail>>,
        ProgramCurrent == LoopStart,
        ProgramLeft == Instruction<PrevInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopStart, ProgramRight>,
            Pushed<ScanBackward, StateTail>,
            Output
        >()[keyPath: keyPath]
    }

    // scan backward to instruction after loopstart, nonnested
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<Step, StateTail>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, Pushed<Step, StateTail>>,
        ProgramCurrent == LoopStart,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<Step, StateTail>,
            Output
        >()[keyPath: keyPath]
    }

}

extension Machine where ProgramCurrent == Exited {
    var output: Output {
        .init()
    }
}

// +++[->+++<]>[->++++>++++++++>+++++++++<<<]>>.+.<----.>>++.++++.<.---.>---.

typealias PrintHi = Machine<
    ToInfinityAndBeyond,
    Zero,
    ToInfinityAndBeyond,
    End,
    Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<LoopStart,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        End>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
Pushed<Step, EmptyStack>,
EmptyStr
>

protocol Infer {
    associatedtype InferredType
    static var inferFrom: InferredType { get }
}
struct PrintHiOutput: Infer {
    static let inferFrom = PrintHi().output
}

print(PrintHiOutput.InferredType.self)
print(PrintHiOutput.InferredType.value)
16 Likes

Pretty sure that I have some Combine Publishers with longer type signatures than this.

19 Likes

My brain wouldn't shut up overnight. A couple improvements:

  • none of these methods are called, so replace the bodies with fatalError()
  • use double-terminators on the program linked lists, to reduce special cases in the VM

Doesn't make much difference to anything, but it's a bit nicer...

protocol Nat {
    static var value: Int { get }
}
struct Zero: Nat {
    static var value: Int {
        0
    }
}
struct Succ<Pred: Nat>: Nat {
    static var value: Int {
        1 + Pred.value
    }
}

/*
print(Succ<Succ<Succ<Zero>>>.value)
*/

// ----

protocol Str {
    static var value: String { get }
}
struct EmptyStr: Str {
    static var value: String {
        ""
    }
}
struct Char<Unicode: Nat, Prefix: Str>: Str {
    static var value: String {
        var result = Prefix.value
        result.append(Character(UnicodeScalar(Unicode.value)!))
        return result
    }
}

/*
typealias A = Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
typealias H = Succ<Succ<Succ<Succ<Succ<Succ<Succ<A>>>>>>>
typealias I = Succ<H>

print(Char<I, Char<H, EmptyStr>>.value)
*/

// ----

protocol MemoryTape {}
struct ToInfinityAndBeyond: MemoryTape {}
struct Square<Value: Nat, Tail: MemoryTape>: MemoryTape {
    var value: Value
    var tail: Tail
}

// ----

protocol Instr {}
protocol SimpleInstr: Instr {}
struct Exited: Instr {}
struct Inc: SimpleInstr {}
struct Dec: SimpleInstr {}
struct Next: SimpleInstr {}
struct Prev: SimpleInstr {}
struct CharOut: SimpleInstr {}
struct LoopStart: Instr {}
struct LoopEnd: Instr {}

// ----

protocol ProgramTape {}
struct End: ProgramTape {}
struct Instruction<I: Instr, Rest: ProgramTape>: ProgramTape {
    var instruction: I
    var rest: ProgramTape
}

// ----

protocol MachineState {}
struct Step: MachineState {}
struct ScanForward: MachineState {}
struct ScanBackward: MachineState {}

protocol StateStack {}
struct EmptyStack: StateStack {}
struct Pushed<State: MachineState, Rest: StateStack>: StateStack {}

@dynamicMemberLookup
struct Machine<
    TapeLeft: MemoryTape,
    TapeCurrent: Nat,
    TapeRight: MemoryTape,
    ProgramLeft: ProgramTape,
    ProgramCurrent: Instr,
    ProgramRight: ProgramTape,
    Stack: StateStack,
    Output: Str
> {

    // increment
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Succ<TapeCurrent>,
            TapeRight,
            Instruction<Inc, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Inc
    {
        fatalError()
    }

    // decrement
    subscript<OutputString, StateTail, Pred, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            Pred,
            TapeRight,
            Instruction<Dec, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Dec
    {
        fatalError()
    }

    // next, existing tape
    subscript<OutputString, StateTail, TapeRightFirst, TapeRightRest, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            Square<TapeCurrent, TapeLeft>,
            TapeRightFirst,
            TapeRightRest,
            Instruction<Next, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeRight == Square<TapeRightFirst, TapeRightRest>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Next
    {
        fatalError()
    }

    // next, creating tape
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            Square<TapeCurrent, TapeLeft>,
            Zero,
            ToInfinityAndBeyond,
            Instruction<Next, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeRight == ToInfinityAndBeyond,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Next
    {
        fatalError()
    }

    // prev, existing tape
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            ToInfinityAndBeyond,
            Zero,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeLeft == ToInfinityAndBeyond,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Prev
    {
        fatalError()
    }

    // prev, creating tape
    subscript<OutputString, StateTail, TapeLeftFirst, TapeLeftRest, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeftRest,
            TapeLeftFirst,
            Square<TapeCurrent, TapeRight>,
            Instruction<Prev, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeLeft == Square<TapeLeftFirst, TapeLeftRest>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == Prev
    {
        fatalError()
    }

    // charout
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<CharOut, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Char<TapeCurrent, Output>
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == CharOut
    {
        fatalError()
    }

    // loopstart, nonzero
    subscript<OutputString, StateTail, Pred, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramCurrent == LoopStart,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        fatalError()
    }

    // loopstart, zero
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<ScanForward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Zero,
        ProgramCurrent == LoopStart,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        fatalError()
    }

    // loopend, zero
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Zero,
        ProgramCurrent == LoopEnd,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        fatalError()
    }

    // loopend, nonzero
    subscript<OutputString, StateTail, Pred, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopEnd, ProgramRight>,
            Pushed<ScanBackward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<Step, StateTail>,
        TapeCurrent == Succ<Pred>,
        ProgramLeft == Instruction<PrevInstr, Rest>,
        ProgramCurrent == LoopEnd
    {
        fatalError()
    }

    // scan forward over simple instruction
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<ProgramCurrent, ProgramLeft>,
            NextInstr,
            Rest,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramCurrent: SimpleInstr,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        fatalError()
    }

    // scan forward over loopstart
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<ScanForward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == LoopStart
    {
        fatalError()
    }

    // scan forward over loopend
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopEnd, ProgramLeft>,
            NextInstr,
            Rest,
            StateTail,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanForward, StateTail>,
        ProgramRight == Instruction<NextInstr, Rest>,
        ProgramCurrent == LoopEnd
    {
        fatalError()
    }

    // scan backward over simple instruction
    subscript<OutputString, StateTail, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<ProgramCurrent, ProgramRight>,
            Stack,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, StateTail>,
        ProgramCurrent: SimpleInstr,
        ProgramLeft == Instruction<PrevInstr, Rest>
    {
        fatalError()
    }

    // scan backward over loopend
    subscript<OutputString, StateTail, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopEnd, ProgramRight>,
            Pushed<ScanBackward, Stack>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, StateTail>,
        ProgramCurrent == LoopEnd,
        ProgramLeft == Instruction<PrevInstr, Rest>
    {
        fatalError()
    }

    // scan backward over loopstart, nested
    subscript<OutputString, StateTail, PrevInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Rest,
            PrevInstr,
            Instruction<LoopStart, ProgramRight>,
            Pushed<ScanBackward, StateTail>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, Pushed<ScanBackward, StateTail>>,
        ProgramCurrent == LoopStart,
        ProgramLeft == Instruction<PrevInstr, Rest>
    {
        fatalError()
    }

    // scan backward to instruction after loopstart, nonnested
    subscript<OutputString, StateTail, NextInstr, Rest>(dynamicMember keyPath: KeyPath<
        Machine<
            TapeLeft,
            TapeCurrent,
            TapeRight,
            Instruction<LoopStart, ProgramLeft>,
            NextInstr,
            Rest,
            Pushed<Step, StateTail>,
            Output
        >,
        OutputString
    >) -> OutputString
    where
        Stack == Pushed<ScanBackward, Pushed<Step, StateTail>>,
        ProgramCurrent == LoopStart,
        ProgramRight == Instruction<NextInstr, Rest>
    {
        fatalError()
    }

}

extension Machine where ProgramCurrent == Exited {
    var output: Output {
        fatalError()
    }
}
/*
// ++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-.<.+++.------.--------.>>+.>++.
typealias PrintHi = Machine<
    ToInfinityAndBeyond,
    Zero,
    ToInfinityAndBeyond,
    Instruction<Exited, End>,
    Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Exited,
        End>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
    Pushed<Step, EmptyStack>,
    EmptyStr
>

print(PrintHi().output.debugDescription)
*/
// +++[->+++<]>[->++++>++++++++>+++++++++<<<]>>.+.<----.>>++.++++.<.---.>---.

typealias PrintHi = Machine<
    ToInfinityAndBeyond,
    Zero,
    ToInfinityAndBeyond,
    Instruction<Exited, End>,
    Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<LoopStart,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<LoopStart,
        Instruction<Dec,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<Prev,
        Instruction<LoopEnd,
        Instruction<Next,
        Instruction<Next,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Next,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<Inc,
        Instruction<CharOut,
        Instruction<Prev,
        Instruction<CharOut,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Next,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<Dec,
        Instruction<CharOut,
        Instruction<Exited,
        End>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
Pushed<Step, EmptyStack>,
EmptyStr
>

protocol Infer {
    associatedtype InferredType
    static var inferFrom: InferredType { get }
}
struct PrintHiOutput: Infer {
    static let inferFrom = PrintHi().output
}

print(PrintHiOutput.InferredType.self)
print(PrintHiOutput.InferredType.value)
4 Likes

Reminded me of my experiment of using "pure" Swift with no standard library or built-ins: first create type "Bit", then "Byte" on top of Bit, then do everything else on top of Byte.

3 Likes

I love it! Great job.

This is a nice discovery.

Have you seen this? Termination checking for type substitution It’s closer to your example in that it encodes a possibly non-terminating computation, rather than an undecidable question per se.

(Also here’s a well-actually: my post from 2020 that you linked technically doesn’t prove Turing-completeness. Nowadays protocols with undecidable word problems (and some with decidable too or course) are rejected during type checking because completion fails, and once completion succeeds we can solve word problems by computing normal forms, which always terminates)

9 Likes

Why even bother with Byte? The obvious next step is arbitrary precision integers using parameter packs.

8 Likes

To be "semi useful" it had to be layout compatible with the rest of the world – hence the need for bytes. Because of layout compatibility constraint I had to do Byte an enum of 256 values instead of a straight tuple of eight bits (although that didn't stop me having back and forth conversions between Bytes and Bits, e.g. to bit shift a byte I converted it to the corresponding tuple, shifted the tuple bits and converted resulting shifted tuple back to Byte.

2 Likes

Share your basic building block code? How do you shift a tuple? Manually?

Yes, basically:

enum Byte { x00, x01, ... xff }
enum Bit { case o, I }

extension Byte {
    init(bits: (Bit, Bit, Bit, Bit, Bit, Bit, Bit, Bit) { ... a giant switch }
    var bits: (Bit, Bit, Bit, Bit, Bit, Bit, Bit, Bit) { ... a giant switch }
}

func bsl_byte(_ a: Byte, _ b: Byte) -> Byte {
    let v = a.bits
    switch b {
    case .x00: return a
    case .x01: return .init(bits: (.o, v.0, v.1, v.2, v.3, v.4, v.5, v.6))
    case .x02: return .init(bits: (.o,  .o, v.0, v.1, v.2, v.3, v.4, v.5))
    case .x03: return .init(bits: (.o,  .o,  .o, v.0, v.1, v.2, v.3, v.4))
    case .x04: return .init(bits: (.o,  .o,  .o,  .o, v.0, v.1, v.2, v.3))
    case .x05: return .init(bits: (.o,  .o,  .o,  .o,  .o, v.0, v.1, v.2))
    case .x06: return .init(bits: (.o,  .o,  .o,  .o,  .o,  .o, v.0, v.1))
    case .x07: return .init(bits: (.o,  .o,  .o,  .o,  .o,  .o,  .o, v.0))
    case .x08: return .init(bits: (.o,  .o,  .o,  .o,  .o,  .o,  .o,  .o))
    default: return   .init(bits: (.o,  .o,  .o,  .o,  .o,  .o,  .o,  .o))
    }
}

More details on the journey in the mentioned thread.

3 Likes

Oh, naming the cases in hex is so much smarter than what I was trying to do in my attempt.

1 Like

And this:

.Ox07

would get you almost normal looking hex integers! :smile:

I wasn't able using normal integer literals in that exercise (no joy of ExpressibleByIntegerLiteral). Also Bool type is not available so instead of normal if condition had to do a more awkward:

enum Bool { case `false`, `true` }
let condition: Bool = .false

if case .true = condition {
    ....
}

Sounds like we can stop looking into compile-time evaluation of constant expressions :sweat_smile: This should do the trick

2 Likes

No, remember that Swift’s generics are not monomorphized. If you can’t get the compiler to print the answer to you in a diagnostic, you don’t have a guarantee that it’s not happening at run time!

5 Likes

And value wouldn't get constant folded either way :cry: (unless the Swift compiler is somehow unwrapping and checking unicode scalars at runtime and evaluating recursive computed properties)

I tried to throw it into godbolt to check. With the flags to extend the compiler's memory and time limit, it took too long and godbolt killed it: Compiler Explorer

1 Like

It does for Succ/Nat, in a release build. But not for Char/Str — it's just too complicated, prepending unicode scalars to strings :woman_shrugging:

3 Likes

Excellent idea! Sadly we cannot involve parameter packs here to build a generic tuple in this way. Wonder if the bar can be lifted, so we can have something like:

protocol Nat {
    associatedtype Tuple<E>
}
struct Zero: Nat {
    typealias Tuple<E> = ()
}
struct Succ<Pred: Nat>: Nat {
    typealias Tuple<E> = (E, repeat each Pred.Tuple<E>)
}

print(Succ<Succ<Succ<Zero>>>.Tuple<Int>.self) // (Int, Int, Int)
1 Like