Archive for the ‘TCS’ Category

QOTD XIV

Monday, July 30th, 2007

From the outside, the type systems of languages like Haskell and ML tend to look like a sort of archaic ecstatic religious rite. The bleeding mendicants pause as they shuffle past, sing a verse in praise of the purifying pain of strong typing, then prod themselves with pointy sticks and progress along their lonely road.

Bryan O’Sullivan, commenting on his own quotation of Yaron Minsky. I’ve heard people complain about Haskell’s type system as being too strict, but once you figure out how to get things to type check, you can actually use it like a miniature theorem prover. Which is, essentially, what it is.

Oh yeah, and it’s my birthday today.

Posted in computing, diary, Haskell, QOTD, TCS | No Comments »

Abstract category theory is like…

Sunday, June 24th, 2007

… writing without nouns.

But ahhh, to write nounlessly is to live anew, not to be tied to thinking concretely, not to be anchored, not to be grounded, but rather to lift off and fly, as if previously to write was just to crawl, penned in, hemmed in, restricted.

And I might add, like an Oasis song, to say everything and yet say nothing. (The traditional way to express this is to call it “abstract nonsense“; the book Abstract and Concrete Categories: The Joy of Cats has this cute limerick which captures the feeling:

There’s a tiresome young man from Bay Shore.
When his fiancée said, “I adore
The beautiful sea,”
He said, “I agree,
It’s pretty, but what is it for?”)

Journal time: I came back from a week back home in Hampshire today, after going with my brother to the Muse concert at Wembley on Sunday. (Woo! That was brilliant!) We also went to a Spanish restaurant for Dad’s birthday, which was pretty tasty.

Our degree results came out yesterday, but I wasn’t around to get them, so I’m having to hold my breath until Monday.

Posted in art, beauty, category theory, diary, music, news, TCS | No Comments »

Milliways and the equivalence of programming languages

Friday, January 26th, 2007

It’s been known since the time of Turing that what’s computable in one reasonably powerful programming language is computable in every other one. As a result, we can say that large classes of programming languages are ‘equivalent’ in the sense that they can emulate each other. However, not all programming languages have natural equivalents of all the others’ features.

This is the idea behind Greenspun’s Tenth Rule:

Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp.

The usual corollary is “including Common Lisp”. We could say the same for C: most C compilers are implemented in C and compile themselves. Similarly, the Glasgow Haskell Compiler is written (mostly) in Haskell. Actually, given that C is the implementation language for so many interpreters, it’s easy to see that one could, in principle, write a program in language X by directly creating the abstract syntax tree and passing it to an “evaluate” function, all in C.


(more…)

Posted in code, computing, Haskell, TCS, thinking aloud | No Comments »

The essence of functional programming

Friday, January 5th, 2007

Here’s an interesting toy language/Turing tarpit for you: Lazy K.


You may already have seen Unlambda, which is essentially the lambda calculus in programming langauge form. (Actually, as its name suggests, it doesn’t actually have any lambdas – it’s really based on the equivalent SKI combinator calculus.) However, Unlambda is a horrible dirty – ahem, I mean impure functional language because 1) it isn’t lazy and so programs in it can sometimes gratuitously fail to terminate, and 2) it has an exception to the evaluation rules (the d ‘function’) and side effects (the .x function prints the character x). Also, in Unlambda version 1 there is no way to do input.


Lazy K is no easier to write programs in than Unlambda (that’s hardly the point, is it? :). But it solves all these problems: it is lazily evaluated; there are no side effects; and you can do input.


(more…)

Posted in computing, TCS, thinking aloud | No Comments »