Haskell IRC

The Haskell IRC channel is great.  For those of you who don't know, IRC is an old school chat room.  The Haskell instance has dozens of knowledgeable people on at any time of day.   They are generous with beginners like me.  I've asked a few dozen questions by now, and always got an answer within a minute or two.  If you're learning Haskell, I highly recommend it.

orangutan and hound

http://www.huffingtonpost.com/2009/09/26/orangutan-and-hound-dog-b_n_299010.html

Yuri

I was at Microsoft Research in Redmond this week.  I met a Russian logician named Yuri Gurevich who told me a funny story about a math class when he was a child:

I remember, in a geometry class, my teacher wanted to prove the congruence of two triangles. Let’s take a third triangle, she said, and I asked where do triangles come from. I worried that there may be no more triangles there. Those were hard times in Russia, and we were accustomed to shortages.

He was afraid they might have run out of triangles!

Good article on Met director

http://www.nytimes.com/2009/09/27/arts/music/27mcgr.html

Alicia de Larrocha's NY Times obituary.

Design Patterns

I've been using Haskell a lot lately.  I wanted a deeper understanding of the interaction of type classes, since the number of type variables in mine is exploding as I try to simulate the ML module system in type classes.  Obviously I'm doing something wrong.  Thus, I've been reading the standard papers on functional dependencies, etc.  For variety, I figured I'd reread some object oriented programming stuff, since they've thought a lot about class relationships.  (Though type classes bear little resemblance to OO classes, there are some similarities.)  So I picked up the Gamma et. al Design Patterns book.  I know I live in a functional programming bubble, but I'm surprised at some of the stuff I'm reading.

  p.22.  On "parameterized types" aka. parametric polymorphism, aka. generics.

  "None of the patterns in this book concerns parameterized types, though we use them on occasion to customize a pattern's C++ implementation.  Parameterized types aren't needed at all in a language like Smalltalk that doesn't have compile-time type checking."

It sounds as if the authors think of compile-time type checking as a scourge on programmers that
forces them to use parameterized types.  
  To be fair, they do say that parametric types are another way (the other two being class inheritance and object composition) to structure your programs, each having strengths and weaknesses.  Interestingly, they point out that you can't change the implementation of a polymorphic function at run time.  That's true (I think) but I'm struggling to understand what they mean.  For instance, you might have two implementations of sorting with different behaviors (e.g. one better on one kind of data, the other on another kind), and you might notice that a chosen sort of an input stream is performing badly and want to switch to the other algorithm.  This is an easy thing to do in ML or Haskell, as I suppose it is in C++.
Thus, I don't know what they mean by saying you can't change the implementation at runtime.  Do they mean, the implementation of a single function?  If so, I have no idea why you would want to do that.  How could you reason about your function f if sometimes it's calling f1 and other times it calls f2?
   The abstractions of design patterns seem interesting, but I'm not seeing yet how to apply the ideas to functional programming.

Babysitting coop

Fascinating story from Paul Krugman:

I like to explain the essence of Keynesian economics with a true story that also serves as a parable, a small-scale version of the messes that can afflict entire economies. Consider the travails of the Capitol Hill Baby-Sitting Co-op.

This co-op, whose problems were recounted in a 1977 article in The Journal of Money, Credit and Banking, was an association of about 150 young couples who agreed to help one another by baby-sitting for one another’s children when parents wanted a night out. To ensure that every couple did its fair share of baby-sitting, the co-op introduced a form of scrip: coupons made out of heavy pieces of paper, each entitling the bearer to one half-hour of sitting time. Initially, members received 20 coupons on joining and were required to return the same amount on departing the group.

Unfortunately, it turned out that the co-op’s members, on average, wanted to hold a reserve of more than 20 coupons, perhaps, in case they should want to go out several times in a row. As a result, relatively few people wanted to spend their scrip and go out, while many wanted to baby-sit so they could add to their hoard. But since baby-sitting opportunities arise only when someone goes out for the night, this meant that baby-sitting jobs were hard to find, which made members of the co-op even more reluctant to go out, making baby-sitting jobs even scarcer. . . .

In short, the co-op fell into a recession.

Self-inforcing protocols

Interesting article by Bruce Schneier:

I especially like the property tax example.

cat flap

I learned this week that Newton invented the cat flap.

LSUIPresentationMode change

I've been using the LSUIPresentationMode trick to hide the Mac toolbar for most applications.  With the latest update, it doesn't look like you can set the number to 4, the options being strings.  You need to now right click and select Show Raw Keys/Values in order to set the number to 4.

Best quote(s) of LFMTP

I think it's a tie

1) Gilles: Higher order matching with dependent types is undecidable.
    Jason: Really?  Who proved that?
    Gilles: I did.

2) Derek: Have you looked at how I do it in MixML?  How do the methods compare?
    Florian: I haven't looked, but I'd be surprised if they are different.  If you do it right, it ends up like this.
   Derek: I was going to say, if you do it right, it ends up like MixML.

Computer security

A British hacker somehow managed to shut down the US Army's computers for 24 hours.
I didn't hear about this.  I thought this comment was interesting.

He had used his own computer with a 56K dial-up modem at his London home with no password protection and somehow managed to evade every security measure the U.S. military had adopted.

70 years seems excessive.  Perhaps the Army should hire this guy rather than put him
in jail. 

Great picture

Haskell 'import qualified'

Haskell's module system is a bit weird.  Consider the following:

import qualified Data.List as L
import qualified Data.Char as L

x = L.concat []
y = L.toUpper 'c'

How can this make sense?  I was interpreting

import qualified Data.List as L

as

structure L = Data.List

in SML.

Apparently the qualified import just makes a new namespace and
dumps all the names from the modules into it.  If there is a conflict,
you simply can't use the name.  For instance, if it was Data.Map and Data.List,
then L.union would be ambiguous.

DMTCP Checkpointing

Checkpointing is the ability to stop a process, save it, and restart it later.  As a user of HOL Light, checkpointing is nearly essential, since every time you start the system it evaluates all of mathematics from scratch.  Loading advanced libraries can take upwards of an hour.  Checkpointing is hard to get right though, and I haven't found a single program that works on the latest Linux kernel.  I started using DMTCP this weekend, and it works perfectly.  I highly recommend it.  The steps are simple.

1) Install DMTCP using a Debian package or from source.
2) dmtcp_checkpoint -n ocaml
3) #use "hol.ml";; (to start HOL Light)
4) dmtcp_command -c (from another terminal.  This checkpoints the process)
5) Kill the ocaml process.  Then do dmtcp_restart on the saved binary.

Works like a charm.

Latex Alert + Array + Infer bug

You can't do the following in Latex:


\documentclass{beamer}
\usepackage{proof}

\begin{document}

\begin{frame}
  \begin{array}{c}
    \alert{\infer{A}{A}}
  \end{array}
\end{frame}

\end{document}

For some reason you can \alert an \infer outside of an \array, but not inside.  Weird bug.

Workaround:  Use tabular instea


\begin{frame}
  \[
  \begin{tabular}{c}
    \alert{\infer{A}{A}}
  \end{tabular}
  \]
\end{frame}

Old Jade and the Zombie!

I'm currently reading

History and Future of Implicit and Inductionless Induction:
Beware the Old Jade and the Zombie!

by Claus-Peter Wirth.  My favorite quote so far:

 In practice, however, refutational completeness by itself does not help in refuting
invalid conjectures or in finding finite proofs for inductively valid formulas.
Only theoreticians completely detached from reality can consider nonterminating
proof attempts in refutationally complete inference systems to be
successful proofs.

Alabama

What is wrong with Alabama?

WTF??

The Senate just passed a bill controlling credit card companies.  What the **** is Tom Coburn thinking?  No wonder people hate Congress.  (Why anyone would need a loaded gun in a national park is a good question, but somewhat beside the point.)

One amendment attached to the Senate bill by Senator Tom Coburn, Republican of Oklahoma, would restore a Bush administration policy allowing loaded guns in national parks. That provision is not in the House version, so there may be discussions between the two chambers over the issue.

BibTeX oddity

Comments don't always work in BibTeX files!  I had the following in my bib file:

@STRING{lncs = {LNCS}}
% @STRING{lncs = {Lecture Notes in Computer Science}}

I wanted the shorter "LNCS" rather than "Lecture Notes in Computer Science".  For some reason, the long form kept showing up in my bibliography.  Transposing the lines gives the desired effect.  Weird...