Hacker News new | ask | show | jobs
by Wazzymandias 3362 days ago
I honestly have no idea what's going on, but his writing is humorous.
2 comments

As far as I can tell, this is an article teaching functional programmers LISP, using the framing of a LISP programmer who trolls a technical interviewer by writing LISP-like Haskell libraries with which to solve the n-queens problem.
This is closer to using the type system to simulate something Prolog-like, where typeclass membership is like a predicate.
I knew that ListConcat looked fishy.
I'm not a Haskell expert (and I skimmed the article), but I believe the article is about designing a simple method of computation that runs on top of Haskell's type system and that operates via type inference.

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

https://en.wikipedia.org/wiki/Kind_(type_theory)

https://en.wikipedia.org/wiki/Peano_axioms

  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?
Yes, and that functional language is LISP, as demonstrated by the parentheses and Cons operator, and a few other things I probably didn't catch. I suppose it's less educational, and more just a meta-level trolling.
Cons is not exclusively a Lisp operation, Haskell's lists (among other languages) are implemented with cons: [1,2] is syntactic sugar for 1:2:(). And the parens are also part of the Haskell syntax, not something added to make it look like Lisp - note the lack of parens around the outermost types.

If anything it seems closest to Idris, given the Peano arithmetic...

I don't think it's actually Lisp. Lisp is essentially an imperative language; you use functional concepts, but you're telling the computer what concrete thing to do at each step. This is just asking it to resolve types in a type system, using whatever algorithm it likes to satisfy the type constraints.

Note, in particular, the complete lack of algorithm to solve the actual n-queens problem: just the constraints.

Fair enough, I pretty much nope'd out after the "Haskell is a dynamically-typed, interpreted language" bit, scrolled to the end, and saw some LISP-y output.
Here's what's going on, as far as I can tell:

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.

What's the runtime?

Zero by the usual definition, but then again it's cheating.

> Zero by the usual definition

Well, one.

He never actually runs the program, he just asks for its type. So zero is defensible.
Fair enough.
Thank you! Your explanation made the most sense, a lot of the other ones went over my head. This is so clever and fascinating.