Makefile for HUnit tests

Here's a nice idiom for running HUnit tests from a Makefile. Jesse Tov gave me the idea that you can use make's dependencies to test only modules that have changed since the last time you ran the tests. Pick a standard name for each module's tests--tests, say--and make sure it's defined in the first column (since we'll be searching for it with a simple grep). Every time we test a module, we'll touch a dummy file of the same name in some hidden directory--call it .test. So we have two lists of files, the modules of the application and the test dummy files:

SOURCES := $(wildcard *.hs) $(wildcard *.lhs)
TESTS := $(foreach src,$(SOURCES),.test/$(src))

To run the tests, first we collect the list of modified modules and save the names of their tests (Foo.tests, Bar.tests, etc.) in a temporary file .test/args.

.test/%hs: %hs
   @if grep '^tests ' $< > /dev/null 2>&1 ; then \
       touch $@ ; \
       echo $* | sed -e 's/\..*/.tests/' >> .test/args ; \
   fi

Now every time we run the tests, we first make a fresh .test/args file, and then we run GHC with a command-line option to evaluate an expression that runs those tests:

test: teststart $(TESTS)
   @echo ghc Test -e "\"Test.run [ `xargs -a .test/args | tr ' '  ','` ]\""
   @ghc Test -e "Test.run [ `xargs -a .test/args | tr ' ' ','` ]"

teststart:
   @mkdir -p .test
   @$(RM) -f .test/args
   @touch .test/args

It's also useful to have a target that always runs all the tests:

retest: testclean test

testclean:
   $(RM) -rf .test

This assumes the existence of a simple test harness module:

module Test (run) where
import Test.HUnit
run :: [Test] -> IO ()
run ts = (runTestTT $ TestList ts) >> (return ())

Some tools just don't like each other

brit·tle, adj.

1. Multi-line string literals in Haskell require so-called "string gaps": one '\' character to terminate a line and another '\' to start the next line.
2. With GHC, Haskell programs may be preprocessed with CPP, which coincidentally strips the "\ ... \" characters from the source, resulting in an illegal Haskell string literal.
3. Mercifully, it also happens that CPP doesn't strip the characters if the first '\' character is followed by a space before the newline.
4. But of course, a commonly used feature of emacs is to silently strip trailing whitespace at the end of lines on every save.
5. Not that you can see the difference, given the well-known human limitations at visually distinguishing whitespace.

(Sensitive types should take this neither as a criticism of GHC nor as implicit condonement of using CPP for Haskell programs--I know it's shunned. You've gotta admit this is beautiful, though.)

When to use point-free style

I've often struggled with the question of when/whether to use point-free style. It can be dangerously addictive, especially in languages with syntactic support for it like Haskell. But it's notorious for creating dense and impenetrable code. Yesterday I linked to advice from the GHC community on when not to create needless abstractions, advice which could be applied when considering a point-free abstraction (man, does it ever take self-restraint not to go wild with the puns here).

The reason why pointful style can be so helpful is it allows us to think about the definition of a computation in terms of particular examples. For any number, let's call it x, ... This is also why set comprehensions in math, and consequently list comprehensions in programming languages, are so approachable: they describe a set by appeal to representative examples.

I think the key to successfully using point-free style is when you want to treat a function itself as a single data point. For example, if you're sorting a list with some comparison function, you don't want to have to drop down a level of abstraction to think about the individual pairs of elements being compared; you just want to think about the comparison function (like "numeric" or "reverse alphabetical") as the object of your attention.

Well said

From the GHC wiki:

It's much better to write code that is transparent than to write code that is short.

Often it's better to write out the code longhand than to reuse a generic abstraction (not always, of course). Sometimes it's better to duplicate some similar code than to try to construct an elaborate generalisation with only two instances. Remember: other people have to be able to quickly understand what you've done, and overuse of abstractions just serves to obscure the really tricky stuff.

Not fade away

From the old-languages-never-die dept.:

Obsolete programming languages such as FORTRAN and COBOL are still widely used.

-- J.J. Duby, 1971

Another cute Haskell function

join :: Eq a => [(a,b)] -> [(a,c)] -> [(a,(b,c))]
join a1 a2 = [ (a,(b,c)) | (a,b) <- a1, c <- [ c | (a',c) <- a2, a == a' ] ]

infixr 5 ⋈
(⋈) :: Eq a => [(a,b)] -> [(a,c)] -> [(a,(b,c))]
(⋈) = join

-- for example:
[("a",1),("b",2),("c",3)] ⋈ [("a",'a'),("b",'b'),("c",'c')]

Crazy debugging feature idea

Here's a crazy idea. Closures are like objects with private fields, right? Specifically, outside of the function body, you're not allowed to refer to the variables in the closed environment. But one of the most annoying things that happen when I'm debugging is that I want to call some local function, but it's not available from the REPL:

(define (foo x y)
  (define (helper z)
    ... x ... y ...)
  ...)

What if, at the REPL (i.e., in debug mode only), closures were openable? You could use dot-notation to refer to them, and all you'd have to do is somehow provide the extra bindings needed to fill in their environment. Keyword arguments, maybe?

> ((close foo.helper [#:x 42] [#:y 'blah]) "value of z")
'result-value-ftw!

Xor

While I'm at it, let's continue the series of logical Maybe operators with xor:

infixr 2 ^^^

(^^^) :: Maybe a -> Maybe a -> Maybe a
Nothing ^^^ r@(Just _) = r
l@(Just _) ^^^ Nothing = l
_ ^^^ _ = Nothing

My current favorite little Haskell function

Here's my pet Haskell combinator du jour:

infixr 2 |||

(|||) :: Maybe a -> Maybe a -> Maybe a
Nothing ||| x = x
x ||| _ = x

This gives you a concise notation for branching in the Maybe monad, so instead of having to write:

case x `lookup` env1 of
 Just v -> Just $ f1 v
 Nothing -> case x `lookup` env2 of
              Just v -> Just $ f2 v
              Nothing -> Nothing

you can write:

do { v <- x `lookup` env1; return $ f1 v } |||
do { v <- x `lookup` env2; return $ f2 v }

This gives you the same kind of idiom that Schemers use or for. Come to think of it, I guess you could also write the analog of and:

infixr 3 &&&

(&&&) :: Maybe a -> Maybe a -> Maybe a
Just _ &&& r@(Just _) = r
_ &&& _ = Nothing

I haven't used this one yet, but it seems natural.

Intentional capture

Procedural hygienic macro systems like the syntax-case system make it possible to write capturing macros--macros which, depending on your philosophy, you might call "non-hygienic." The classic example is the "anaphoric" conditional form if-it, which implicitly binds a variable it to the result of the test expression:

(if-it 42 (+ it 1) #f) ; => 43

The difficulty in getting such a macro right comes when you try to write another macro that expands into if-it. To quote the mzscheme manual's section on macros, "macros that expand into non-hygienic macros rarely work as intended."

Andre van Tonder's SRFI 72 document contains a perfect and concise example, due to Kent Dybvig, of two different ways a macro might expand into a capturing macro. On the one hand, we might want to write when-it, a simple "one-armed" conditional that implicitly binds it in the same way as if-it:

(when-it 42 (+ it 1)) ; => 43

On the other hand, we might want to use if-it to implement the hygienic or macro, which shouldn't capture any variables.

(let ([it 10]) (or #f it)) ; => 10

First, here's the implementation of if-it: we create an identifier for it with the same lexical context as the operator of the expression:

(define-syntax (if-it stx)
  (syntax-case stx ()
    [(op e1 e2 e3)
     (with-syntax ([it (datum->syntax #'op 'it)])
       #'(let ([it e1])
           (if it e2 e3)))]))

The references that will be captured by the introduced binding of it are the ones that were introduced into the program in the same expansion step as the occurrence of if-it in the macro call. In particular, if the occurrence of if-it was in the original program (i.e., written explicitly by the programmer), it captures references to it that were in the original program; if the occurrence of if-it is the result of a macro expansion, it captures only those references to it that were generated in that same expansion step.

This means that a hygienic macro that expands into if-it will work as expected:

(define-syntax or
  (syntax-rules ()
    [(op e1 e2)
     (if-it e1 it e2)]))

Since the reference to it appears in the same expansion step as the occurrence of if-it, that reference is captured, but no references to it within subexpressions e1 or e2 (which had to have already been there before this expansion step) are captured.

If you want to write another capturing macro that expands into if-it, it's a little more work. Essentially, you have to capture it all over again. The moral of the story is that you always have to ask explicitly for a macro to capture an introduced identifier.

(define-syntax (when-it stx)
  (syntax-case stx ()
    [(op e1 e2)
     (with-syntax ([it* (datum->syntax #'op 'it)])
       #'(if-it e1 (let ([it* it]) e2) (void)))]))

Here we once again create an identifier with the same lexical context as the operator, and we bind it to the occurrence of it introduced by if-it.

These are good defaults for a hygienic macro system: it's easier to write hygienic macros but still possible (albeit a little harder) to write macros that capture. This is even true when you abstract over capturing macros: macros that expand into capturing macros are hygienic by default, but with a little more work again, you can create capturing macros that abstract over other capturing macros.

True unions

I am a Super Big Fan of disjoint union datatypes in programming languages, but there are places where they are really inconvenient. Having to inject and project data between related types can be prohibitively cumbersome, especially when dealing with large data definitions such as the AST definitions for realistic programming languages. I know of a couple of languages where "true" unions are used instead, including Typed Scheme and the draft ECMAScript Edition 4. In both cases, unions are being added to a language where the runtime is already paying the price for runtime type tags, so keeping the variants distinct where they don't overlap doesn't introduce any extra burden.

But I was thinking this morning, what would happen if you tried to add true unions to Hindley-Milner languages? For concreteness, let's imagine extending Haskell. So instead of writing

data Foo = I Int
         | S String

you could instead write

type Foo = Int | String

Now if you want to pattern match on such a construct, you have to explicitly mention the type; there's no other way to distinguish the variants. So you could imagine type-annotating the patterns in a match expression:

showFoo :: Foo -> String
showFoo foo = case foo of
                n :: Int -> show n
                s :: String -> s

Note that because there's nothing prevent overlap in the variants of a true union, the order in which you match the patterns is significant. Alternatively, you could write the definition of showFoo in pattern-definition style:

showFoo :: Foo -> String
showFoo (n :: Int) = show n
showFoo (s :: String) = s

Consider the possible drawbacks to such a feature:

Cost of tagging:

One of the benefits of (sound) static typing is the ability to compile to efficient runtimes that avoid tagging runtime objects with their datatype. The Foo type, by contrast would require its Ints and Strings to be tagged. But this is the wrong way of looking at it; the language requires you to tag them anyway if you use the disjoint union type, so there's no additional cost over what you would already have been paying. For non-union types, you can still do the same amount of erasure.

Possible overlap:

You can express overlapping types like (Int | (Int | String)) with true unions, which makes the order of patterns significant, could result in surprising (order-dependent) logical relationships between case dispatches, and could generally lead to messy type definitions. Maybe a more principled way of looking at it is a disjoint union can be thought of as a type abstraction, whereas with a true union you might have to know its full definition to use it effectively. But hey, the same is true of type-definitions but they're still useful; and besides, nothing's preventing you from using disjoint unions when they're more appropriate.

Case exhaustiveness:

Standard ML's pattern matching facility is carefully designed to allow the compiler to prove or disprove case exhaustiveness. I tend to think this is a bad trade-off; the language is significantly crippled to enable a very weak theorem prover to prove a theorem that's of limited utility. Sure, it has its uses, but when you know things the theorem prover doesn't, you have to abandon pattern matching entirely. Other language designers seem to agree with me, since Haskell and I think Ocaml also don't check for case exhaustiveness.

Inference problems:

I have no expertise in Hindley-Milner inference, but I'm sure true unions are not inferrable. But one thing recent Haskell research has demonstrated is that convenient but uninferrable extensions to Hindley-Milner type systems can often be safely added with the requirement that they be explicitly annotated. I bet you could add true unions, require explicit type annotations when they're used, and get along just fine.

Function types and polymorphic types:

This is where it gets tougher. How do you tag these kinds of types? Do you do runtime subtyping checks for things like the more-polymorphic-than relation? I don't have an answer. A simple one is to restrict unions to types with simple tags, although those kinds of arbitrary restrictions lead to lack of compositionality in language design. But perhaps it's possible to make this work with the entire type system.

Some of this design space has been explored with Ocaml's polymorphic variants. I should take a look at the literature on that.

Thank heavens for PLT v4

I've just finally installed my first pre-release of PLT v4 (actually v3.99.0.9 at present), and there are so many little conveniences that are already qualitatively improving my life. Here are a few of the ways v4 is making me happy:

automatic opt-lambda: As I understand it, the underlying low-level #%plain-lambda is like the original lambda, but in the full scheme language, the automatically available, high-level lambda has support for the functionality of opt-lambda from the old (lib "etc.ss") library. More often than not, that was the only reason I needed to require that library. It's so nice just to be able to reach for opt-args right away, without having to jump through any extra hoops.

keyword integration: Moreover, the high-level lambda also has automatic support for keyword arguments! This means there's a very smooth evolution path for functions: 1) positional when you just need a few arguments; 2) optional when one or two of them have reasonable defaults; and 3) keywords when there are enough arguments with enough defaults that it's too hard for the user to remember their order.

built-in pattern matching: No need to require (lib "plt-match.ss") -- it's already in the full scheme language by default. I stumbled on that by accident!

generalized define-struct: There used to be a huge gap between what you could do with define-struct and what you could do with the very general but hard-to-use make-struct-type. But thanks to the expressivity of keywords, the new define-struct form is much more powerful. Plus it's so much easier to understand what

(define-struct posn (x y) #:transparent)

means, as opposed to

(define-struct posn (x y) #f)

built-in list libraries: Many more commonplace list operations are just automatically there when you use the full scheme language, such as foldl, foldr, last, andmap, ormap, build-list, etc. It used to be confusing trying to remember what was in (lib "list.ss") and what was in (lib "list.ss" "srfi" "1"). Now, if I'm not mistaken, I just don't ever need (lib "list.ss") anymore.

my first two columns are mine again: Last but not least, the new #lang module declaration form means I no longer have to indent the entire body of a module.

It looks like the PLT crew have really worked hard on fixing lots of these little inconveniences (some of which I only noticed consciously now that I no longer have to deal with them!).

The Culpepper Method of Good Writing

Ryan Culpepper's algorithm for good writing:

Blather. Condense. Repeat.

König's Lemma

How do you show that a simulation preserves non-termination? I think you could probably use coinduction, but I'm not very familiar with coinductive arguments. I just learned about a useful result called König's Lemma, which I think allows you to use a simple induction.

Let's say we have a simulation relation e′ ~ e ("e′ simulates e") and a proof that for any step in a specification semantics:

e₁ → e₂

we have related terms e₁′ ~ e₁ and e₂′ ~ e₂ such that

e₁′ →⁺ e₂′

It's easy to show by induction that if the specification semantics converges to a value then the implementation semantics converges to a related value. If the specification semantics diverges, i.e. has an infinite reduction sequence, then we'd like to show the implementation diverges too.

König's Lemma states that for any finitely branching tree, if there exists a path of length n from the root for any n, then there exists an infinite path from the root. Consider the tree of possible reduction sequences from a term, where branches indicate points of non-determinism in the semantics. If every point of non-determinism has only a finite number of alternative reductions, then the tree is finitely branching.

So now consider a diverging term e in the specification semantics. For any finite prefix of the infinite reduction sequence, we can easily show by induction that there is a reduction sequence in the implementation semantics of equal or greater length. Since the computation tree of the implementation term is finitely branching, König's Lemma provides an infinite reduction of the implementation.

Two optimizations, only one safe

PLT Scheme's module system suggests some simple compiler optimizations. For one, identifiers bound in a module cannot be mutated from outside the module. This makes it very easy to determine whether the binding is immutable: just scan the source for instances of set!. If there aren't any, you can rely on the binding's immutability for optimizations like constant propagation.

Here's another tempting one: if a module imports a library but doesn't use some of the library's exported bindings, it seems like it should be safe not to load those bindings, right? Nope! Because the macro system has complete access to the syntactic environment, a macro exported by the module might actually compute a reference to the binding:

(define-syntax (foo stx)
  (syntax-case stx
    ... (datum->syntax-object
          #'here
          (string->symbol "mumbly-foo")) ...

The syntax object #'here encapsulates the entire syntactic environment, and if the imported library exports mumbly-foo, looking up 'mumbly-foo in the syntactic environment will find it. Similarly, run-time code in the module might perform

(eval (datum->syntax-object #'here 'mumbly-foo))

and it would again find the binding. So it's not generally possible to prune any library imports, as long as macros and eval have complete access to the syntactic environment through syntax objects.

Well, eval is scary... does this mean the first optimization is unsafe, say, if eval tries to mutate it? I don't think so. Module bindings are stored in the lexical (i.e., local) environment, which I believe is not available to eval. The bindings available to eval are the ones that come from PLT Scheme's "namespace" objects. As I understand it, these namespaces do not contain mappings for local variables, only for globals and module imports.

Up for air

It's been a busy month! Last week I got back from ICFP in lovely Freiburg, Germany, where I gave a talk about my functional pearl as well as a status report on the JavaScript reference implementation. ICFP was a blast--I can't count the number of cool people I got to meet, hang out with, trade ideas with, argue with, and drink delicious German beer with. Then as soon as I got back to Boston, I had just a week to finish my submission to ESOP with Mitch on our theory of hygienic macros.

Science and engineering

Joel Spolsky has a post about the phases of the software development cycle that's remarkably close to my own observations. In Joel's view, the first phase is art (i.e., design phase); the second is engineering (construction); and the third is science (debugging and testing).

Joel's interest is in project management and management tools, but mine is more in development tools. Once you recognize the divide between the engineering and science aspects of software development, you can better understand one of the tensions in the approach to development, a tension which leads to plenty of heated debate. This tension comes about because the Fundamental Immutable and Inviolable (Not to Mention Sacred, Holy, and Good) Laws of Engineering are sometimes at odds with the practice of science.

To wit: abstraction and modularity are the heart and lungs of software engineering. Rules #1 , 2 and 3 are "Localize concerns, i.e. Don't Repeat Yourself, separate concerns and enforce their orthogonality." More simply: use abstractions and don't violate them. By making one concern completely oblivious to (i.e., parametric in) another, you maximize your freedom to change one without affecting the other. This allows for local reasoning which in turn leads to separable development and maintenance. Disciplined developers create layered abstractions and fastidiously respect their boundaries.

But what happens when you start debugging? Dogmatically adhering to abstraction boundaries is like wearing blinders; when a bug first arises, you never know which abstraction layer it's hiding in, or if it's in the interaction between layers. Another common consequence of thinking inside the abstraction box is impulsively assuming the bug is someone else's fault. ("The compiler must be broken!") I'm reminded of Knuth's quote about computer scientists:

Such people are especially good at dealing with situations where different rules apply in different cases; they are individuals who can rapidly change levels of abstraction, simultaneously seeing things "in the large" and "in the small."
          -- quoted in Hartmanis's Turing Award lecture

I think this is describing more the science and perhaps also the design aspects--but not the engineering aspect--of software development.

Because debugging and testing are about observing and understanding an existing system, rather than constructing or modifying a system, the barriers we construct to enforce our engineering principles become obstacles. Debugging tools, IDE's, testing frameworks, etc. are all characterized by a need to violate abstraction boundaries.

As a result, the Cleans and Dirties (as Mitch calls them) fight tooth and nail about whether our software development frameworks should be absolutely strict in their adherence to the FIaI(NtMSHaG)LoE (ML) or absolutely lax (Smalltalk). I wonder if we couldn't do better by building software frameworks that were aware of these different modes of development.

Progress is what matters

It's a well-known slogan in PL theory circles that Type Soundness = Preservation + Progress. But sometimes, people just write the Preservation lemma. Sometimes they even confuse type soundness with type preservation. Richard and I were chatting today and he reminded me that the goal of a type soundness theorem is to guarantee the absence of runtime type errors. In that sense, just proving that expressions remain well-typed is skipping the punch-line. The Progress lemma tells you that, assuming you're well-typed, you'll never get stuck with a type error--that's the point!

Real-world trace analysis

Robert O'Callahan has just released a debugger called Chronomancer, which is based on a technology he's been working on for a little while: Chronicle is a database for storing and querying program events, built on top of Valgrind, a dynamic analysis tool that instruments Linux binaries to monitor their runtime behavior. Chronomancer is a C/C++ debugger deployed as an Eclipse plug-in. There's a rough screencast here, though I didn't follow everything he was doing.

One of the cooler aspects of the debugger is the idea of history-based stack reconstruction. There's a tug-of-war that goes on between debuggers and compilers: compilers want to mess with data structures and control that is not supposed to be observable to programs, and debuggers want to observe them! As a result, there's constant disagreement or confusion about the interface between the two, resulting in impartial stack information or corrupted debugging information. Chronicle avoids these issues by relying on the history of events, rather than the stack layout, to determine what calls have happened when, and which ones have returned. This means, for example, that tail calls don't interfere with stack traces, because stack traces are based on program history instead of continuations.

The song that doesn't end

M Ward's song Chinese Translation sounds like an MIT AI koan from the 70's:

I met an old, old man
beneath a weeping willow tree
He said now if you got some questions
go and lay them at my feet...

And I said
What do you do with the pieces of a broken heart...

...and then the sun went down
and he sang for me this song

See I once was a young fool like you...
I met an old, old man
he sat beneath a sapling tree
He said now if you got some questions
go and lay them at my feet...

And I said
What do you do with the pieces of a broken heart...

The song ends before we reach a base case, but notice the trees get smaller, so there might be an inductive measure after all.