[jcrites]

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

[mrkgnao]

  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?

[jldugger]

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.

[couchand]

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...

[geofft]

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.

[jldugger]

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.