peteg's blog

Graham Greene: The Quiet American

/noise/books | Link

Much better than the movie led me to believe. (I must have seen it at the cinema back in 2002 or so). There's a great article at Literary Traveller about how the locations in the novel map to modern-day Hồ Chí Minh City. Specifically rue Catinat is now Đồng Khởi.

Control

/noise/movies | Link

I guess this movie had to be be made, after 24 hour party people. David Bowie's Aladdin Sane makes a welcome appearance (and noise) in the opening scenes.

As you'd expect from Corbijn, the cinematography is beautiful, with many segments being moving photographs (where the camera has a fixed focus).

I quite enjoyed it after waiting more than six months to see it, though as a biography it felt a bit hollow.

Mulholland Drive

/noise/movies | Link

Not David Lynch's finest. I enjoyed the linear-plot bits, and there are some beautifully shot scenes... but as I recall from seeing it in the cinema so many years ago, it's not a patch on Blue Velvet.

Pierre Brocheux: Hồ Chí Minh

/noise/books | Link

Somehow I got the idea that there was such a thing as Hồ Chí Minh's autobiography in print [*], and I've made sporadic efforts to find it over the past six months or so. It turns out I should've looked harder on the internet, as I would have found the Communist Party of Vietnam's extensive stash of his papers.

Anyway, while in Sydney I bought this book on a whim, largely because it seemed to be the best thing that the UNSW Bookshop had on the big man. It really is quite a disappointing work, though; the reviews on Amazon and in the Times Higher Education do a good job of explaining why.

So I guess I'm still looking for a book that tries to explain what Bác Hồ had in mind for Việt Nam, and how things have actually played out.

[*] This is somewhat like my attempts at finding the ABBA museum in Stockholm in 2004. Hmm, perhaps there is one now...

Simplifying the XHTML DTD for fun and profit.

/AYAD/Project | Link

For the usual reasons it seemed best to use FCKeditor as an input widget for HOPE. I had hoped to provide some kind of hacker-friendly markup but time is short and convincing FCKeditor to generate it would probably require some heart surgery. So XHTML everywhere it is.

Clearly this path should lead to paranoia; we can't allow users to submit arbitary strings, or even arbitary XHTML. My heavyweight solution is to validate such submissions against a stripped-down XHTML DTD using HaXml. So far I've removed forms, scripts and restricted the attributes of <a> to just href. I wish the DTD was readable; it is merely an algebraic data type afterall.

Combined with some thorough string-escaping for the other inputs and a tendency to cop-out (crash) on anything that doesn't completely conform to expectations, I think we will be all right.

You can try your hand here. Any and all feedback is much appreciated.

In related news I've uploaded my FCKeditor "server-side integration" Haskell library to Hackage. Find that here.

The Secret Life of Words

/noise/movies | Link

Chinatown

/noise/movies | Link

A Kangaroo comes to Vietnam

/noise/theatre | Link

Some performance art by a Vietnamese bloke who spent some time in Australia, part of the celebration of thirty-five years of diplomatic relations between Australia and Vietnam. Loan and I went along in the spur-of-the-moment.

Griffith Review #19: Re-imagining Australia (Autumn 2008)

/noise/books | Link

Hey, here's an idea: let's publish a journal on the future of Australia, now that it has one... I know, we can invite some ALP has-beens and let them run rampant with triumphal gushings. Let's also get someone to flog that republican horse one more time!

This is the weakest Griffith Review I've read yet. A significant portion of this journal is dedicated to dancing on the graves of the culture warriors who have apparently lost due to John Howard's election defeat. (It is news to me that they were winning before.) To someone who has very limited interest in the history wars, these are wasted pages; indeed this edition feels more like an exploration of Australia's past, and is a bit short on ideas for the future.

Skipping lightly over the articles that failed to excite, these were worth the read:

  • Tom Morton's Dreams of Freedom, though really just an advertisement for his upcoming book on Georg Forster, intriguingly portrays the Enlightenment ideals and aspirations at the time of Britain's discovery of Australia.
  • Bruce Elder trekked out west to Hungerford and wrote In Lawson's Tracks. Of course Henry Lawson suggested a better name would have been Thirstyford... There's not much meat on the bone in this piece, which illustrates the argument Lawson and Banjo Paterson had over the nature of the bush by quoting them as extensively as the space limit allowed. It is a pleasant amble, though.
  • Marcia Langton's essay Trapped in the Aboriginal reality show is a compelling call to action. However to a non-specialist it is difficult to understand who (substantively) she is disagreeeing with, and so the false dichotomies (symbolic versus "practical" issues, for example) are irritating clangers.
  • Listening is harder than you think, Kim Mahood's essay about her involvement with a remote Aboriginal community, is the kind of thing I buy Griffith Review for: direct, personal reportage with some perspective thrown in, without overwhelming ideology.
  • Jenny Bowler's memoir Mungo memories is a quiet celebration of her father's life's work, and I wish there were more pieces like this. Australia has loads of world experts in all sorts of arcana, and it would be good to hear about them more regularly.
  • Similarly Barry Hill documents his father's industrial relations (unionist) expertise in A letter to my father.
  • Wayne McLennan returns with another great piece of writing, Meat. He's got a tidy set-piece at the end of the first section:

    "What are you, a wog or something?"

    "He's Dutch [...] and so am I", I lied, "so shut your fucking mouth."

    [...] "What's going on?" C asked.

    "Australian egalitarianism," I answered. "We like everybody to be the same as us."

    I'm going to have to check out his books.
  • Maria Tumarkin's article Life in translation is in the same vein as Peter Mares's one from the previous edition, taking aim at an immigration department that seems thoroughly resigned to wasting human capital.
  • I liked Oren Seidler's A new land, 1976, though it is fizzy and rotted my teeth.

Matrix Revolutions

/noise/movies | Link

The Matrix Reloaded

/noise/movies | Link

Withnail and I

/noise/movies | Link

The Three Burials of Melquiades Estrada

/noise/movies | Link

Trung Nguyên: 301B An Dương Vương, District 5.

/AYAD/HCMC/Cafes | Link

Fellow-and-soon-to-be-ex-AYAD Yen steered me to this seedy old man's café quite near my usual and increasingly dear 603. While ancient, I wasn't calcified enough to last long at this place. They only serve the one type of Trung Nguyên coffee, which is a bit punk.

Café Du Miên, 48/9A Hồ Biểu Chánh, District Phú Nhuận.

/AYAD/HCMC/Cafes | Link

Chị Lan (my AYAD In-Country Manager) took us to this café on our first morning in Hồ Chí Minh City, way back in July 2007. It's a friend of Cà Phê Thềm Xưa. I went there today with Loan. We played a few games of Carcassonne (which I'd given her for her birthday) and chatted about xe ba bánh.

Offside

/noise/movies | Link

Vale, 1 Trần Hưng Đạo.

/AYAD/HCMC/Cafes | Link

Well, somewhere in Hồ Chí Minh City a contract quietly expired and the Trung Nguyên at 1 Trần Hưng Đạo in District 1 is no more. The love heart on the front door and Trung Nguyên paraphernalia have been removed.

I now reside at 603 Trần Hưng Đạo, on the edge of District 1. Unfortunately they don't do food.

Once Upon A Time In America

/noise/movies | Link

The Boondock Saints

/noise/movies | Link

Some of Jeremy Gibbons & Graham Hutton's Proof Methods for Corecursive Programs in HOLCF.

/hacking/isabelle | Link

I abandoned this attempt at mechanising a proof of the "approx lemma" about eighteen months ago, for what now seem like spurious reasons; what I had was quite close to what was needed. I was initially interested in the "take lemma" made famous by Richard Bird & Philip Wadler, and how it took the magic step from assertions about finite lists to ones about possibly infinite objects. Well, I definitely feel some awareness of vacuity now.

You can read it here.

The magic is how the continuity underpinning the semantics of functions is reflected into the term language. As such it's unbelievably cute. The proof of correctness is not particularly interesting though, except perhaps as an exercise in fiddling with fixpoints and continuity.

The Matrix

/noise/movies | Link

Bill Roscoe's almost-book on Denotational Semantics.

/hacking/isabelle | Link

Tim pointed this almost-book out to me. It's sorely disappointing that whoever-it-was who should've cranked the operational semantics half did not do so; what is there is top-notch, especially the chapters on Information Systems. Whereas Glyn Winskel's text does a great job of presenting the mathematics of these "concretised" domains, this book also delves into the philosophical concerns and hence makes the mathematics that much easier to follow.

It's linked from near the top of his publications page.

Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, partially.

/hacking/isabelle | Link

It's about time I pushed this out the door. Their proofs went through fine for the most part, except for the need to do some induction when rewriting the recursive calls. It is unclear to me how to prove the lemma that justifies this step in general, though for each instance the induction is quite straightfoward, and the key lemmas for the inductive steps are given in the paper. In effect we need induction just to convince HOLCF, not an optimisation phase, but it would be nice if their fusion rule handled this for me. (My proposed, unproven variant can be found in worker_wrapper.thy.)

I believe there was a small strictness bug in their streams / memoisation example. Score one to HOLCF.

I also tried to mechanise Andy Gill's nub example, which mostly went OK, modulo proving some auxiliary lemmas. Specifically, as above one needs to use induction to rewrite the recursive call, and coming out with the right statements is made difficult by HOLCF's admissibility requirements. A work in progress. Again, I can feel Larry Paulson laughing at me for wasting my time.

You can look at it here, or utter:

darcs get https://peteg.org/isabelle/worker_wrapper/

Note some proofs are quite rough, though most of the important stuff is as clear as Isar. The Nat theory may end up being interesting, though with too much more monadic machinery one may as well use HOL... and I have begun to realise that proof-reuse for even something as simple as lists is quite difficult. There are at least two mainstream types (fully lazy and fully strict), as well as some in-betweens that might be convenient (e.g. head-strict and tail-strict). The code here just begins down the mainstream-Haskell path; I figure the Standard ML people are wise enough to be using HOL or Coq or whatever in the first place.

Royal Tenenbaums

/noise/movies | Link

Kyle used to go on about this movie. I sort-of get it now.

Trung Nguyên: Corner of Hồng Bàng and Đồ Ngọc Thạnh, District 5.

/AYAD/HCMC/Cafes | Link

A small corner-café in the west of District 5 (aka Chợ Lớn and Chinatown). Nothing especially remarkable, except for being on a big fat noisy road.