Typing the technical interview
aphyr.com
aphyr.com
https://aphyr.com/posts/340-reversing-the-technical-intervie...
“You’re… defining the natural numbers by hand? Why?”
“Haskell is for mathematicians,” you explain. “We always define our terms.”
That's just beautifulLike I said earlier in the "half-dead chicken thread", the occult is a quiet and powerful force in computer science and related areas. With things like neural networks and learning functions, we're approaching the ultimate.
In this case, it was only a handful of lines of a functional language that could solve the N-Queens problem.. Of course, mixed with a bit of Lovecraftian lore and Norse magic.
It's only a careful look beneath the stolid atheism and antitheism that the tech community likes to front.. All is not as it appears just beneath the digital waves, is it?
[I think I coined this one, back in the day. But I was probably preceded by someone even more damaged]
Of course, maybe your comment above was playful and ironic as well, in which case I missed the point :)
If you enjoyed that you might enjoy the structure of the proof of the complexity of type inference for \-calculus: http://www.cs.brandeis.edu/~mairson/Papers/jfp02.pdf . They construct arbitrary boolean circuits from simple types and evaluate the circuits through type checking.
You smile kindly. “Haskell is a dynamically-typed, interpreted language.”
Thou shalt not suffer a witch to live!Coincidentally, I had Bach's E minor organ sonata on in the background, so...
> You sigh contentedly.
I did, I started smiling from ear as soon as I read the now-classic "Summon a ______ from the void". :)
Also, TIL: https://en.wikipedia.org/wiki/Sei%C3%B0r
This is a polemic against people who don't know Haskell. Previous iterations were the same except Clojure/Lisp.
Aphyr/Kyle is a genius, and one of my favorite people on the internet. But this series is the WRONG way to attack the code interview, which deserves to be attacked, BUT.
Some of us face real challenges about how to find common ground with interviewees. Because you know you're smarter than those questions is not a reason to discount them.
I will sacrifice ALL my HN points to say this is bullshit. Bullshit written in decent prose, but still bullshit.
Now if you mean that making fun of the coding interview itself is wrong because there exist people who either interview people for a living or people who are job-hunting right now, and this makes light of their troubles, well, that's different. I disagree, but it's still more sensible than "lol you dont know Haskal, nub".
the coups de grâce!!!
Holy shit
import Data.List (permutations)
solve :: Int -> [[Int]]
solve i = filter (valid . zip [1..]) (permutations [1..i])
valid :: [(Int, Int)] -> Bool
valid [] = True
valid (x:xs) = singleValid x xs && valid xs
where
singleValid x xs = all (pairwiseValid x) xs
pairwiseValid (x1, y1) (x2, y2) = abs (x1-x2) /= abs (y1-y2)Seems to not be very bug-ridden either. But maybe somebody should code a non-backtracking operator extension for GHC. This way, next time he could claim Haskell is a dynamically typed, interpreted, lazy and not-pure language.
Haha, that's a good one. Haskell, unlike SML, is _not_ formally specified. If only, if only... sobs
I do think datalog semantics composes way nicer than prolog though.
I think some of the type class stuff was formalized in the papers on HM(X) , though the combination of extensions in this post hasn't. But perhaps should be on the table for formalization.
The answer at the end is evaluated by asking Haskell to print out the type of the variable "solution", and the answer is encoded within that variable's type (rather than its value).
In Aphyr's meta-language, "values" are represented by Haskell types, "functions" are represented by Haskell type constructors (functions from types to other types), and "computation" is represented by type inference.
For example, a cons cell in a typical language is a data structure consisting of two elements, so in Aphyr's meta-language it's represented as the binary type constructor `data Cons x xs`.
The meta-language also defines its own natural numbers and arithmetic in the fashion of Peano arithmetic. `data Z` declares a type that will represent the zero value, and `data S n` declares a unary type constructor representing the successor function. For example, zero is the type `Z`, one is the type `S Z` ("the successor to zero"), two is the type `S (S Z)` ("the successor to the successor to zero"), etc. Using this construction we can build arithmetic recursively. For example, equality in Peano arithmetic is implemented in Aphyr's program as:
class PeanoEqual a b t | a b -> t
instance PeanoEqual Z Z True
instance PeanoEqual (S a) Z False
instance PeanoEqual Z (S b) False
instance (PeanoEqual a b t)
=> PeanoEqual (S a) (S b) t
You can read that code as if it approximately means the following (pseudo-code, bit hand-wavy): function PeanoEqual a b
PeanoEqual(0, 0) = True
PeanoEqual(a+1, 0) = False
PeanoEqual(0, b+1) = False
PeanoEqual(a, b) = # a and b are both nonzero
PeanoEqual(a-1, b-1) # so recurse
My pseudo-code expresses equality of natural numbers by recursively subtracting 1 (that is, undoing our successor function) from `a` and `b` until one of the values is zero. If both are zero, then the original inputs were equal; otherwise they were unequal. In the Haskell meta-program, we don't have imperative recursion, but have recursive types and subtype relationships, and unification that understands them and will construct those types.Further reading:
https://wiki.haskell.org/Constructor#Type_constructor
Note, in particular, the complete lack of algorithm to solve the actual n-queens problem: just the constraints.
If anything it seems closest to Idris, given the Peano arithmetic...
PeanoEqual(a, b) = # a and b are both nonzero
PeanoEqual(a-1, b-1) # so recurse
Subtracting Peano literals would involve some constraints in the type, so shouldn't that be (a+1,b+1) for typing purposes?A "class" in Haskell is a typeclass, sort of like a trait in Rust or an interface / abstract class in OO languages. An "instance" is a specific data type that satisfies the rules of the typeclass. The classic example is something like this:
class Eq a where
(==) :: a -> a -> Bool
instance Eq Integer where
x == y = <some native code>
That is, Eq is a class we can apply to any type a, as long as we have a way of defining the (==) operator, which takes two things of type a and returns a bool. We would like to say that Integer is an instance of this typeclass Eq.You can use classes to express rules about multiple types, by just adding more type variables to the class definition. The Haskell wiki gives the example of matrix and vector multiplication, with "class Mult a b c", "instance Mult Matrix Matrix Matrix", and "instance Mult Matrix Vector Vector".
(One of the problems that comes up when doing this is that type inference doesn't know how to resolve overloaded types. FunctionalDependencies lets you add the "| a b -> c" syntax, which means "the type c in this typeclass is uniquely determined by whatever the type of list is, nobody can instantiate this typeclass twice for the same type of a and b". But don't let that syntax confuse you into thinking that a function, in the normal sense of something taking inputs and producing outputs, is being defined; it's just defining relationships between objects. almost Prolog-style.)
What he's doing is defining type classes for what us normal people would think of as functions. Nil and Cons are separate, unrelated types: in C++ terms, Nil would be class Nil {}, and Cons would be template <typename x, typename xs> class Cons {}. Keep in mind that x and xs are type arguments, not actual data members!
Then there are typeclasses with no functions; nothing needs to be implemented to be a member of the typeclass, but the type constraints need to be satisfied.
So we say that the two types a=Nil and b=Nil satisfy the "First" typeclass, and that the two types a=Cons x more and x also satisfy the "First" typeclass, for any type x (and any type more).
Then ListConcat gets to type constraints: the three types (Cons a as), bs, and (Cons a cs), taken together, satisfy the typeclass ListConcat as long as the three types as, bs, and cs also satisfy it. So now we're asking the type inference algorithm to start doing some recursion and probably some backtracking, but it's all hidden.
So on and so forth, with Peano integers and everything else, until we get to the meat of the queens problem: an instance of the 6-queens problem can be constructed if there are six queens not attacking each other.
Then he asks the typesystem to run type inference and figure out a plausible type for the 6-queens problem.
What's the runtime? Who knows.
Zero by the usual definition, but then again it's cheating.
Well, one.
Like music/art/religion/gourmet-cooking/morris-dancing/synchronized-swimming.
If it's "your thing", it's _wonderful_. It might not be your thing, and that's fine too.
If you're exclusively a bro-country fan, you probably don't appreciate jazz or classical - and that's OK, I hope you get immense joy from your bro-country music.
But that's not necessarily what interviewing is all about. Type-level programming is cool but wildly inappropriate for most jobs - that's part of the humor.
You are not your job, or your resume, or your ability to pass an interview. There are all sorts of ways people can be elite that are mostly orthogonal to a particular job.
This is about wasting an interview demonstrating a semi-obscure technique that's fascinating but mostly useless, and it gets widely praised.
Seems like it's just that fantasizing about turning the tables on an interviewer is fun, never mind whether it makes sense or not.
It obviously draws on some commonly identifiable tech interview tropes, and that's what gives it its comedic value, but I don't it intends to say that the way the witch deals with those interviews is the model way.