Swift has a hole — a little type-driven development

I love Swift’s type system. First when I switched from Objective-C, which was around two years ago, I was so spoiled by dynamic approach from its predecessor that I felt really uncomfortable. After a few hours of writing Swift I was pretty tired. I had to go by its rules and surrender to the type system but it wasn’t long until I stopped fighting it and just followed its advice. We developed a bond. Nowadays I feel like we are good friends.
My appreciation for statically typed languages has been growing steadily since I became more experienced with Swift. I can’t imagine writing any code without static analysis and compile time checks any more. Even when scripting in Python, writing some Bash utilities I somehow feel scared to run the thing without any proof of its correctness.
Recently I stumbled upon a fantastic book from Edwin Brady — Type-driven development with Idris. Edwin is a creator of Idris, a purely functional language. In first chapter of the book, he explains how the name of the book is not a coincidence and is indeed poking at popular approach Test-driven development. In TDD we write tests first. Tests allow us to design flow of the data without much focus on implementation details. Same goes for Edwin’s idea but instead of writing tests we write functions first that accept and return types. Idris has a strong type system and its emphasis on Type-DD is not surprising. Its selling feature are dependent types. Edwin presents a few really simple examples where getting types right lets us implement the feature while type system holds us tight so we won’t do anything stupid. In order to satisfy a type system without finalizing our implementations he introduces a hole. Hole is a placeholder which can be of any type you need and its type is inferred by the type system. Its purpose is to let you draft a function and quickly jump to the next context and just postpone its implementation.
For some time while writing Swift I have been using a really similar pattern where I would use a fatalError in order to silence the compiler.
func numberOfChildren(inRooms rooms: [Room]) -> Int {
fatalError()
}Above code compiles and compiler won’t complain because fatalError calls abort() and it is aware of the termination of program. But what if we could satisfy a compiler and still run it? I thought it is a pretty good idea and tried to mimic a hole concept from Idris. I created AHole. It is a really simple hole implementation. There is only one public protocol AHoleType and a public function _hole_()
func _hole_<A: AHoleType>(file: StaticString = #file,
line: UInt = #line) -> A { print(“AHole: Using a hole for type \(A.self) at line \(line) in file \(file)”)
return A.holed()
}
In repository there is a second file which has a few Foundation types conforming to AHoleType. You can easily extend conformance to your own types and use AHole in your application. I have added a convenience print which will notify you where and for which type a hole was put inside your code.
Happy hole’ing.
