N-Queens, But Make It Type-Level
Technical interviews often hinge on how well a candidate can implement a known algorithm in an unfamiliar setting. Less common, but far more memorable, is the approach of redefining the problem entirely.
Given a chessboard of size NxN, the N-Queens puzzle asks for a placement of N queens so that no piece threatens another—same row, column, or diagonal. The conventional solution involves backtracking through position lists and validating each potential move at runtime.
One alternative: skip the runtime entirely. Instead of writing a function that computes a valid arrangement of queens, encode the queens as types and let the compiler verify the solution. The puzzle stops being a search problem and becomes a proof obligation. If the code compiles, the placement is valid by construction.
Setting the Stage
The script begins with familiar foundations. Lists are defined inductively: a Nil constructor for the empty list and a Cons constructor that prepends a value. This is the standard linked list structure, hand-rolled on the whiteboard, with no reliance on the host language's built-in list syntax.
The class keyword declares a typeclass, essentially a function signature at the type level. Two instances provide the recursion: pattern matching on the list constructor chooses which instance applies. A recursive typeclass constraint appears on the right side of the arrow—implication at the type level, where the presence of a constraint like ListConcat before is required to obtain ListConcat after. This is the type-level analogue of a recursive function call, with the Nil case as the base of the recursion.
Booleans follow in the same self-contained fashion. Two constants—call them True and False—are created to represent the two states. Natural numbers come next via a Peano construction: Zero as the base, and a successor constructor to represent every positive integer.
A Dynamically-Typed Interlude?
At this point, the interviewer asks the obvious question: why are there no type declarations on the functions? The answer, delivered with complete seriousness, is that the language is dynamically typed and interpreted. This claim gets tested immediately.
Expressions like comparing one == one return the expected boolean. But the real test comes from asking what happens when evaluating an invalid comparison, like comparing a True value against a list. The code still loads without complaint. The interpreter balks only when forced to evaluate the expression—an artifact of lazy evaluation, where type checking is deferred until a value is actually demanded. The result is technically a runtime type error, though the error message does not label itself as such.
A comment is made about the notorious opacity of error messages in such systems.
Partial Application, Curried by Hand
Moving on, the conversation turns to higher-order functions. The claim that the language has no built-in currying leads to constructing the tools by hand. A general signature for single-arity application is introduced: a function f applied to an input a yields a result r.
Rather than building a whole family of datatypes for partial application—called Partial1, Partial2, and so on—an explicitly curried version of each needed function is defined directly. One such example is a well-known higher-order function for mapping a function over a list. The recursion proceeds through the type-level list structure, threading functions through each element.
Queens as Types
With the foundations in place—lists, booleans, naturals, and higher-order type-level functions—the actual queens can be introduced. A queen is defined by its x and y coordinates on the board. A partially-applied constructor produces a queen at a given x-coordinate, allowing shorter type expressions.
Queens in this model menace their neighbors in all eight directions. A queen at a given x-coordinate is safe if there is no existing queen on the same row, or in any diagonal position, given a horizontal and vertical displacement. The threat check is itself a type-level computation over the list of previously placed queens.
The key predicate checks whether a given (x,y) coordinate pair is legal relative to an existing list of queens. The recursive structure walks the list, computing per-queen safety. When combined with a universal quantifier over elements—a function that applies a test to every entry in a list—the safety check forbids a placement if any existing queen is within striking distance.
The construction then steps through the columns of the board, maintaining a list of queens placed so far. At each arrival of a potential new position, a candidate coordinate is generated and tested. If no conflicts arise, the new coordinate is appended and the process recurses to the next column. The final arrangement is a simple enumeration: one queen per column, every placement checked and verified at compile time.
A few awkward seconds lapse, during which one participant produces all of the code in the frozen void of a delayed laptop display. But eventually, a valid configuration emerges. Reading off the diagonal, the output shows queens at coordinates like (5,1), (4,3), (3,3), and so on—a clean type level solution. The final expression instantiates this composite type in main, which proves that the board has a satisfying state.
The printout even looks correct when formatted as text: a diagonal of zeroes marching upward in the queen coordinates.
The Verdict
The interviewer manages a long stare. The noticeable point, delivered after a considerable pause, is that a concrete value was never written anywhere. The entire "program" has run at the type level only, with no value inhabiting the result type.
"No, that doesn't sound right," is the only available retort. The follow-up line is predictable enough: we will be in touch.
A test harness written entirely in types, where compiler errors are tantamount to wrong answers, compiles cleanly. That is not worse—it is simply a different definition of what an interview exercise means by solving a problem.
