Wednesday, January 14, 2015

IPv6 seen in the wild!

Don't ask how I got here, but I was looking at the revision history of a Wikipedia page and saw:

(cur | prev) 16:20, 18 December 2014‎ 2607:f470:8:b044:3d66:5782:2dba:2c8b (talk)‎ . . (9,582 bytes) (0)‎ . . (→‎Dialethiesm may be a more accurate model of the physical world) (undo)
(cur | prev) 00:14, 30 November 2014‎ 2601:e:8100:701:4124:33e5:9859:fc9d (talk)‎ . . (9,582 bytes) (-19)‎ . . (→‎Fixed ) (undo)

Yep, those are IPv6 addresses, doing minor edits on a Wikipedia page. Hell hath frozen over and the future is here.

This officially marks the first time I've seen IPv6 used for something other than testing IPv6 or demonstrating IPv6, or demonstrating that someone is an IETF wank.

Wednesday, December 17, 2014

Haskell's biggest flaw

And then a great, deep voice, like as that of James Earl Jones, spake unto me, saying,

The greatest flaw of Haskell is the inability to define the identity function in a point-free style.

Monday, December 1, 2014

Quote o' the day: uh....

From bestpcinfos on Hacker News:

Don't forget to put the tarp over the ham basin before departing for olfactory shoes.

I've got no idea what it means, but it does sound like good advice.

Saturday, November 22, 2014

Link o' the day: How I start—Haskell

Chris Allen has a very good walk-through for starting Haskell programmers (and for projects using cabal): How I Start: Haskell.

(Hey, wha'da'ya' want? It's NaNoWriMo and I'm way behind. And busy.)

Thursday, October 30, 2014

Turing machines vs. other models of computation

Every once in a while, I hear someone complain about the fascination with Turing Machines, in comparison with other models of computation such as lambda calculus, general recursive functions (well, ok, maybe not that one), etc.

The following is Philip Wadler's answer, from "Propositions as Types", an otherwise equally good paper:

Turing’s most significant difference from Church was not in logic or mathematics but in philosophy. Whereas Church merely presented the definition of λ-definability and baldly claimed that it corresponded to effective calculability, Turing undertook an analysis of the capabilities of a “computer”—at this time, the term referred to a human performing a computation assisted by paper and pencil. Turing argued that the number of symbols must be finite (for if infinite, some symbols would be arbitrarily close to each other and undistinguishable), that the number of states of mind must be finite (for the same reason), and that the number of symbols under consideration at one moment must be bounded (“We cannot tell at a glance whether 9999999999999999 and 999999999999999 are the same”). Later, Gandy [16] would point out that Turing’s argument amounts to a theorem asserting that any computation a human with paper and pencil can perform can also be performed by a Turing Machine. It was Turing’s argument that finally convinced Gödel; since λ-definability, recursive functions, and Turing machines had been proved equivalent, he now accepted that all three defined “effectively calculable”.

In other words, a Turing Machine is built for an argument based on the capabilities of a human being, making the argument that it encodes effective calculation stronger. As in Gödel's case, it is not clear that lambda calculus does encode effective calculation.

Further, the Turing Machine formalism has a number of immediately-obvious extensions, such as multiple tapes, that are easily proven to be equivalent to the original machine. As a result, the subsequent, loose, argument that it is closed in power above further strengthens its argument.