vvv's shared items
This neat video about "Radio Hams" from 1939 has recently been circulating on the ham email lists. It's neat to see the excitement and sense of adventure that people had for hacks or "kinks" as they called it way back when...
Read more | Permalink | Comments | Read more articles in Retro | Digg this!We have some sort of machine that prints out statements in some sort of language. It needn't be a statement-printing machine exactly; it could be some sort of technique for taking statements and deciding if they are true. But let's think of it as a machine that prints out statements.
In particular, some of the statements that the machine might (or might not) print look like these:
| P*x | (which means that | the machine will print x) |
| NP*x | (which means that | the machine will never print x) |
| PR*x | (which means that | the machine will print xx) |
| NPR*x | (which means that | the machine will never print xx) |
For example, NPR*FOO means that the machine will never print FOOFOO. NP*FOOFOO means the same thing. So far, so good.
Now, let's consider the statement NPR*NPR*. This statement asserts that the machine will never print NPR*NPR*.
Either the machine prints NPR*NPR*, or it never prints NPR*NPR*.
If the machine prints NPR*NPR*, it has printed a false statement. But if the machine never prints NPR*NPR*, then NPR*NPR* is a true statement that the machine never prints.
So either the machine sometimes prints false statements, or there are true statements that it never prints.
So any machine that prints only true statements must fail to print some true statements.
Or conversely, any machine that prints every possible true statement must print some false statements too.
|
Order 5000 B.C. and Other Philosophical Fantasies ![]() with kickback no kickback |
The conclusion then translates directly: any machine or method that produces statements about arithmetic either sometimes produces false statements, or else there are true statements about arithmetic that it never produces. Because if it produces something like NPR*NPR* then it is wrong, but if it fails to produce NPR*NPR*, then that is a true statement that it has failed to produce.
So any machine or other method that produces only true statements about arithmetic must fail to produce some true statements.
Hope this helps!
(This explanation appears in Smullyan's books 5000 BC and Other Philosophical Fantasies, chapter 3, section 65 (which is where I saw it) and also in The Mystery of Scheherezade.)
I gratefully acknowledge Charles Colht for his generous donation to this blog.
[ Addendum 20091214: Another article on the same topic. ]
As was discussed at the 2009 Kernel Summit, NVIDIA hardware requires the downloading of a large binary blob to function. This blob was taken from NVIDIA's proprietary drivers. Nobody really knows what it is (though most guess that it is firmware), and nobody knows what sort of copyright restrictions might apply to it. So, for now, nobody's really willing to sign off on it for merging into the mainline. As a result, this blob is not part of the new tree; potential users will have to obtain it separately. Even this way, though, the merging of Nouveau would make it more visible and, hopefully, encourage more testing and development.
Update: Linus did pull the Nouveau tree into the mainline.
A fascinating article by Oleg Kiselyov on delimited continuations:
We demonstrate the conversion of a regular parser to an incremental one in byte-code OCaml. The converted, incremental parser lets us parse from a stream that is only partially known. The parser may report what it can, asking for more input. When more input is supplied, the parsing resumes. The converted parser is not only incremental but also undoable and restartable. If, after ingesting a chunk of input the parser reports a problem, we can `go back' and supply a different piece of input.
The conversion procedure is automatic and largely independent of the parser implementation. The parser should either be written without visible side effects, or else we should have access to its global mutable state. The parser otherwise may be written with no incremental parsing in mind, available to us only in a compiled form. The conversion procedure relies on the inversion of control, accomplished with the help of delimited continuations provided by the delimcc library.
I’ve been reading about Haskell quite a bit during the last months, writing some actual code, and liking the language more and more. After many years favouring dynamically typed languages, i’m beginning to really appreciate Haskell’s type system and the benefits it brings to the table.
A common argument from the static typing camp is that the compiler is catching a whole class of bugs for you, to which dynamic types answer that a good test suite (which you need anyway for any serious development) will catch those relatively trivial bugs for you. I tend to agree with the dynamic faction on this issue, but then i think that the strength of static typing (coupled with good type inference) is not at all about the compiler catching typing bugs but, rather, as enforcing useful constraints. When you write Haskell, you have to think hard about your data types and the functions using them; and the compiler will keep complaining and, most importantly, the code will feel awkward and somehow ad hoc until you find a good set of types to solve your problem.
The limits to your freedom imposed by the type system entail, in my experience, a boost in the amount of thought and imagination that i put in my design and implementation, in much the same way as the constraints imposed by metric and rhythm to poetic writing boost creativity and actually help producing a beautiful text. Or, in fact, in the same way as any kind of constraint in any creative endeavour helps (paradoxically, at first sight) in attaining beauty, or, at least, in having fun during the process.
In my experience, the process of writing a program or library in any language is always a struggle to find the right way of expressing the solution to a problem, as the culmination of a series of approximations. The code feels better, more expressive and easy-flowing with each rewrite, until something just clicks and i get this feeling that i’ve finally captured the essence of the problem (a litmus test being that then it’s natural to extend the solution to cases i hadn’t thought of when writing the solution, as if, somehow, the new solutions were already there, waiting for you to discover them). And i’m finding that the powerful type system offered by Haskell (think not only of vanilla Hindley-Milner, but also of extensions such as GADTs or type families) is helping me reaching the (local) optimum quicker, that satisfying constraints means i’m closer to the final solution when my code compiles for the first time. You often hear Haskell programmers saying something similar (“once my code compiles, it works”), and i think it’s mostly true, except that the real reason is not that the compiler is catching trivial typing bugs, but, rather, that the constraints imposed by the type system are making you think harder and find the right solution. Same thing with monads, and the clean separation they provide for stateful computations: again, you must think carefully about the right combination of monads and pure code to solve the problem, and most of the time your code will simply not type check if you don’t get the solution right.
There are two more ways that Haskell’s type system is helping me writing better programs. Two ways that are especially poignant when the code becomes sizeable enough. The first one is self-documentation: seeing the type of my functions (or asking the interpreter for them) instantly informs me of almost everything i need to know to use them; in fact, when writing in dynamic languages i keep annotating function signatures with this same information, only that there i’m all by myself to ensure that this information is right. PLT contract system is but a recognition of the usefulness of typing in this regard, although i much prefer the terseness and notational elegance of Haskell’s type signatures over the much more verbose and, to my eyes, somewhat clunky notation used by PLT (which is not really PLT’s fault, being as it is a very schemish notation). Let me stress here that having a REPL such as ghci is a god-send (and, to me, a necessity for really enjoying the language): it will tell me the type of an expression in much the same way as decent Lisp or Scheme environments will report a function’s signature.
The second way Haskell’s lending a helping hand with non-trivial code base is refactoring. As i mentioned above, i rewrite my programs several times as a rule, and rewrites almost always involve modifying data structures or adding new ones. As i grow older, i find it more and more difficult to keep in my head all the places and ways a given data structure is used in my programs, and with dynamic languages i’m often falling back to grepping the source code to find them. And again, their plasticity often works against me, in that they let me use those data structures in crooked ways, or forget to take into account new fields or constructors for a modified data type. Haskell’s compiler has proved an invaluable ally to my refactorings and, by comparison, modifying and maintaining my bigger dynamic programs is not as fun as it used to be.
As an aside, types are not the only thing i’m finding enjoyable about Haskell. Its astonishing capabilities to express very abstract problems with a remarkable economy of expression (due, in part, to its highly tuned syntax) are extremely useful. To my mind, they mimic the process by which in math we solve harder and harder problems by abstracting more and more, cramming together more relevant information in less space (some cognitive science writers will tell you that thought and even consciousness consists on our ability to compress information). That means that i can express my solutions by capturing them in very high level description: initially, that makes them harder to understand, but once i feel comfortable with the basic concepts and operations, they scale up much, much better than more verbose, less sophisticated ones. Using these new hard-earned concepts, i can solve much harder problems without adding to the complexity of the code in a significant way (one could say, using a loose analogy, that the solutions grow logarithmically with complexity instead of polynomically or exponentially). A direct consequence of this expressiveness is that some well-written Haskell programs are, hands down, the most beautiful pieces of code i’ve ever seen (just pick a random post at, say, a Neighbohood of Infinity and you’ll see what i mean; or read Richard Bird’s Sodoku solver and compare his solution with one written in your favourite programming language).
Finally, let me say that i find programming in Haskell more difficult than programming in any other language i’ve used, with perhaps the only exception of Prolog. Sometimes, considerably so. And that’s perfectly fine with me. For one thing, it makes it more interesting and rewarding. In addition, i’m convinced that that’s the price to pay for being able to solve harder problems. I take issue with the frequent pleas to the effect that programming should be effortless or trivial: writing good programs is hard, and mastering the tools for doing it well takes, as with any other engineering or scientific discipline, hard work (why, i don’t heard anyone complaining that building bridges or computing the effects of gravitational lensing is too difficult). There’s no silver bullet.
All that said, please don’t read the above as an apostasy letter announcing the embracement of a new religion. There’s still much to be said in favour of dynamic languages, specially those in the Lisp family, whose malleability (fostered by their macro systems) is also a strength, in that they allow you to replicate some of the virtues i’ve been extolling in this post. Haskell lacks the power of homoiconicity, its template mechanisms feeling all but cranky, and that’s a serious drawback in some contexts (i have yet to decide how serious, as i have yet to decide how much i’m missing in reflection capabilities). As always, it is a matter of trade-offs and, fortunately, nobody will charge you for high treason for using the language better fit to the problem at hand, or so i hope.
Posted in Essays, Haskell
This evening, Matthew Podwysocki drew my attention to an amusing article over on Phil Trelford's blog, in which people compare various versions of an algorithm for producing left-truncatable primes.
I can't resist a round of golf, and I was of course tempted by Matt Curran's 17-line Haskell entry, so here's the exact same algorithm in 6 lines of Haskell.
ltps = take 4260 $ ps 1 [0]
where
ps m prev = prev ++ ps (m*10) cur
where cur = concat [filter isPrime (map (+n*m) prev) | n <- [1..9]]
isPrime 1 = False
isPrime x = null (filter ((==0) . mod x) [2..floor . sqrt $ fromIntegral x])
To my mind, this is easier to read than the 17-line version, since it more directly expresses what the algorithm actually does.
Phil posts measurements of times to produce the 1000th left-truncatable prime, but this number is so easy to compute that I don't trust the measurements (if you measure something once, and it takes a handful of milliseconds, choose a bigger problem!). Here are the times required on my laptop for Haskell and C++ to compute the 2800th such number, which incidentally requires 64-bit arithmetic to represent:
Haskell: 1.703s
C++: 1.225s (requires most the
ints in the code to turn intolongs to give a correct answer)
The Haskell number isn't bad, given the compactness of the code, the 10 minutes I worked on it, and my total disinterest in working on the problem any further
Folllowing an idea by Kai Hendry, I re-implemented my Linux application screen-message, which does nothing but display a piece of text that you enter as large as possible, in HTML. So whenever you are in need of screen-message, but don’t have it installed at the moment, put your browser into fullscreen mode, go to
and type away.
I only tested it with the web browser galeon, so I expect it to work with Firefox and related browsers. If it does not work with Internet Explorer, I can’t help it – but patches are welcome. The file is stored in the screen-message Darcs repository at http://darcs.nomeata.de/screen-message.upstream.
PS: If anyone wants to donate a shorter domain for this, you are welcome. But I guess all good domains with “sm” in them are taken...

