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!
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?!
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!
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)
Compiling main.swift (56s)
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