Computer Science Education Week

In honor of Computer Science Education Week, I'll just cite a passage I find inspirational about the role of computer science education:

Yet programming is more than just a vocational skill. Indeed, good programming is a fun activity, a creative outlet, and a way to express abstract ideas in a tangible form. And designing programs teaches a variety of skills that are important in all kinds of professions: critical reading, analytical thinking, creative synthesis, and attention to detail.

We therefore believe that the study of program design deserves the same central role in general education as mathematics and English. Or, put more succinctly,

everyone should learn how to design programs.

On one hand, program design teaches the same analytical skills as mathematics. But, unlike mathematics, working with programs is an active approach to learning. Interacting with software provides immediate feedback and thus leads to exploration, experimentation, and self-evaluation. Furthermore, designing programs produces useful and fun things, which vastly increases the sense of accomplishment when compared to drill exercises in mathematics. On the other hand, program design teaches the same analytical reading and writing skills as English. Even the smallest programming tasks are formulated as word problems. Without critical reading skills, a student cannot design programs that match the specification. Conversely, good program design methods force a student to articulate thoughts about programs in proper English.

From "How to Design Programs," by Felleisen, Findler, Flatt and Krishnamurthi.

Ezra: Function calls are not stack frames

I don't have much to add to this but Ezra's saying things that are true:

Tim Bray is spreading more misinformation about tail recursion. He describes it this way:

It looks like a subroutine call, but in the case where it occurs as the last thing in the routine, it magically, silently, and automatically gets turned into, now how did I put it? “A highly controlled and structured GOTO.”

A tail-call is a subroutine call. The efficient implementation does not magically transformed into something else; if it doesn't create a stack frame on such a call, it's because one simply isn't relevant.

It's worth reading Ezra's whole post. I especially appreciate his point about confusing semantics with cost model.

Proposed json.plt change

I'm not sure how many users I have of my json.plt PLaneT package, nor how many of them read my blog. But I thought I'd see if I could take a straw poll here. I'm thinking about changing the data definition in a backwards-incompatible way. What if I said:

A jsexpr is one of:

• 'null
• boolean
• string
• integer
• inexact-real
• (vectorof jsexpr)
• (listof (cons symbol jsexpr))

The nice thing about this representation is that it's easier to quote and quasiquote. The down-sides are that array manipulation is a little less convenient, and table lookup is slower.

Another alternative is:

A jsexpr is one of:

• #:null
• boolean
• string
• integer
• inexact-real
• (listof jsexpr)
• (listof (cons symbol jsexpr))

The nice thing about this is that both arrays and tables are conveniently represented as lists. But it's a little uglier for representing null, which is necessary to avoid ambiguity between the JSON strings { "null" : [] } and [[null]]. Note that it's also a little more subtle to distinguish between arrays and tables.

Other possible unambiguous representations of null include #\null, #"null", or #&0. Yech.

If you have any opinions, feel free to comment here or email me privately.

Update: Whoops, can't have them both be lists, because of the ambiguity between the empty object and empty array.

Mitchfest blog

We've created a Mitchfest blog where we'll be posting updates on new material as it becomes available, including presentation slides, videos, and publication of issues of the Festschrift.

Quote of the day

"What's surprising to me is that this language ever managed to achieve widespread use - but I guess it's just another example of how you can break a whole bunch of precious rules and the sky doesn't necessarily fall in. Software is full of people declaiming their 'thou shalt not' lists, and right across the street there's another bunch of people breaking those very rules quite profitably."
-- Daniel Earwicker

Mitchfest program

We've posted the Mitchfest schedule and program!

Call for Participation: Scheme Workshop 2009

[Note: only one day left to register! --Dave]

2009 Workshop on Scheme and Functional Programming
Co-Located with the Symposium in Honor of Mitchell Wand

August 22, 2009
Boston, Massachusetts, USA
http://www.schemeworkshop.org/2009

CALL FOR PARTICIPATION

To the delight of all and sundry, the 2009 Scheme and Functional Programming Workshop will be held on August 22nd at Northeastern University, and it is a signal honor for me to be able to invite YOU to the WORLD'S FOREMOST WORKSHOP on the marvelous Scheme language, and to present a program PACKED with contributions from familiar faces and new ones, certain to amaze, delight, and edify. Lend us your ears, and we will widen the space between them.

- John Clements

IMPORTANT DATES

August 11, 2009 - Registration deadline
August 22, 2009 - Workshop on Scheme and Functional Programming
August 23-24, 2009 - Symposium in Honor of Mitchell Wand

VENUE

Northeastern University
Boston Massachusetts
Curry Student Center Ballroom (Building 50)
346 Huntington Ave
Boston, MA 02115

ACCOMMODATION

A limited block of hotel rooms has been reserved for participants of the Scheme Workshop and/or the Mitchell Wand Symposium at hotels in Cambridge and Boston. See the workshop web site for more information, and please note that some of these special rates have already expired.

REGISTRATION

The registration fee will be $40 to help cover the operating costs and lunch accommodations. Please register by August 11, 2009 so that we will have an accurate head count. To register, please send an email to aoeuswreg@brinckerhoff.org with your name and any dietary restrictions for lunch.

PROGRAM COMMITTEE

• John Clements (Cal Poly State University (organizer & chair))
• Dominique Boucher (Nu Echo)
• Abdulaziz Ghuloum (Indiana University)
• David Herman (Northeastern University)
• Shriram Krishnamurthi (Brown University)
• Matthew Might (University of Utah)
• David Van Horn (Northeastern University)

PRELIMINARY PROGRAM

Invited: If programming is like math, why don't math teachers teach programming?
Emmanuel Schanzer

Invited Talk on Future Directions for the Scheme Language
The Newly Elected Scheme Language Steering Committee

The Scribble Reader: An Alternative to S-expressions for Textual Content
Eli Barzilay

World With Web: A compiler from world applications to JavaScript
Remzi Emre Başar, Caner Derici, Çağdaş Şenol

Scalable Garbage Collection with Guaranteed MMU
William D Clinger, Felix S. Klock II

Distributed Software Transactional Memory
Anthony Cowley

Sequence Traces for Object-Oriented Executions
Carl Eastlund, Matthias Felleisen

Keyword and Optional Arguments in PLT Scheme
Matthew Flatt, Eli Barzilay

Fixing Letrec (reloaded)
Abdulaziz Ghuloum, R. Kent Dybvig

Descot: Distributed Code Repository Framework
Aaron W. Hsu

A pattern-matcher for miniKanren -or- How to get into trouble with CPS macros
Andrew W. Keep, Michael D. Adams, Lindsey Kuper, William E. Byrd, Daniel P. Friedman

Randomized Testing in PLT Redex
Casey Klein, Robert Bruce Findler

Screen-Replay: A Session Recording and Analysis Tool for DrScheme
Mehmet Fatih Köksal, Remzi Emre Başar, Suzan Üsküdarlı

Interprocedural Dependence Analysis of Higher-Order Programs via Stack Reachability
Matthew Might, Tarun Prabhu

Get stuffed: Tightly packed abstract protocols in Scheme
John Moore

Higher-Order Aspects in Order
Eric Tanter

Peter J Landin (1930-2009)
Olivier Danvy

Selectively disabling tail recursion

The anti-tail-recursion crowd often complains about loss of information in stack traces. In DrScheme, if you raise an exception after a sequence of tail calls:

(define (fact-iter n acc)
  (if (zero? n)
      (error 'fact "stop!")
      (fact-iter (sub1 n) (* n acc))))
(fact-iter 3 1)

the stack trace you get back has very little information in it.

One argument you'll sometimes hear from people like me is that in a properly tail calling language, you can always turn a tail position into a non-tail-position, whereas the reverse is impossible. But in practice, when you want broadly better diagnostics, manually converting lots of individual function calls throughout a program is too hard to be practical, and you then have to go and undo it afterward.

So in the spirit of linguistic tools for diagnostics, I've discovered a dirt-simple trick for improving the information in stack traces while debugging.

PLT Scheme lets you hijack the normal meaning of function application by rebinding the #%app macro. So I defined a utility called trace-app that wraps its function application in (roughly) the identity function, forcing the given function call out of tail position. Then all you have to do is add to the top of a module:

(require (planet dherman/tail:4))
(define-syntax #%app trace-app)

and suddenly, all function applications that occur syntactically within the current module body are non-tail calls, and voilà:


Update: I've posted a new version of the package, which exports trace-app in a slightly different way. The initial version had a hazard that client modules which used

(provide (all-defined-out))

would inadvertently re-provide #%app, which would then disable tail recursion for its client modules.

The new way to use it is

(require (rename-in (planet dherman/tail:5) [trace-app #%app]))

or

(require (only-in (planet dherman/tail:5) [trace-app #%app]))

Linguistic tools for diagnostics

I've written before about how the stack gets misunderstood as a history thanks to non-tail-recursive languages. Of course, stack traces are indispensable: they're essential for debugging, and they're also useful for reporting crash information from live applications.

But this conflates two very different language requirements in one feature: the need for nested (unbounded, if your language isn't broken) function application, and the need for diagnostics of dynamic errors.

The first is what continuations and stacks are all about, of course: functions can't call each other function calls can't be nested in compound expressions without the language runtime keeping track of the work it has left to do. But the second is an independent need: there's all sorts of diagnostic information that's potentially useful, and the stack just happens to be one source of information that's already there.

Now, as it turns out, it's a pretty useful source of information. And if you happen not to have proper tail recursion, it's even more useful, since it provides a path through the function call graph. But I've been finding stack traces in Scheme less informative, because with proper tail calls, there's less function-call history in the continuation.

I recognize that sometimes the "complexity budget" in language design necessitates using one feature to satisfy multiple requirements. But I'd like to see more investigation of linguistic diagnostics designed independently of existing language features. For example, it might be useful to provide configurable tracing facilities that record program history during runtime, where the tuning of how much gets recorded is completely independent of the space semantics of the evaluator. So you have a properly tail recursive semantics with a flexible tracing facility grafted on top.

What classifies a language feature as "purely diagnostic" might be that it is designed not to change the observable behavior of the program, but merely to report some additional information. Contracts-as-projections is an example.

Update: rephrased my rookie characterization of continuations.

Contractiveness not required for regularity

Yesterday I wrote about ensuring termination of subtyping for equirecursive types that I thought contractiveness ensures that the (potentially) infinite tree corresponding to a recursive type is regular. That was wrong. Contractiveness just ensures that you can't represent types that don't have a corresponding tree, such as μA.A. The fact that the tree is regular comes from the fact that the syntactic representation is finite and substitution doesn't add anything new.

Regular => Subtree set finiteness => Termination of memoized algorithm

The termination argument behind the TAPL algorithm for subtyping of equirecursive types is not as scary as it sounds (or as it sounded to me, anyway). It's as simple as this: even though the subtyping rules generate bigger types when they substitute a recursive type into its own body, the fact that the types are regular means that there are only a finite number of distinct subterms in the infinite type tree--that's the definition of regular trees. So as long as you keep a cache of types you've looked at before and never have to look at the same pair of types twice, you can't do an infinite number of checks.

(Eventually, you run out of work.)

If I'm not mistaken, the syntactic restriction that types are contractive, i.e., recursive type variables have to appear under constructors, is sufficient to guarantee that the corresponding type trees are regular.

Call for Participation: Symposium in Honor of Mitchell Wand

Symposium in Honor of Mitchell Wand
In Cooperation with ACM SIGPLAN
Coordinated with Scheme Workshop 2009

August 23-24, 2009
Boston, Massachusetts, USA
http://www.ccs.neu.edu/events/wand-symposium

CALL FOR PARTICIPATION

IMPORTANT DATES

August 1, 2009 - Registration deadline
August 22, 2009 - Scheme Workshop
August 23-24, 2009 - Symposium in Honor of Mitchell Wand

VENUE

Northeastern University
346 Huntington Ave
Boston, MA 02115 USA

ACCOMMODATION

A limited block of hotel rooms will be reserved for participants of the Symposium and/or the Scheme Workshop at hotels in Boston and Cambridge. More information will be available soon; please check back on the event web site.

REGISTRATION

Registration is free. Please register by August 1, 2009 so that we will have an accurate head count. To register, please send an email to mitchfest-registration@ccs.neu.edu with your name and any dietary restrictions for lunch.

SCOPE

Northeastern University is hosting a special Symposium in celebration of Dr. Mitchell Wand's 60th birthday and honoring his pioneering work in the field of programming languages. For over 30 years Mitch has made important contributions to many areas of programming languages, including semantics, continuations, type theory, hygienic macros, compiler correctness, static analysis and formal verification.

Please join us at Northeastern on August 23rd and 24th as we celebrate this personal milestone and pay tribute to a great computer scientist, researcher, teacher and colleague, Dr. Mitchell (Mitch) Wand.

STEERING COMMITTEE

* Olivier Danvy (University of Aarhus)
* David Herman (Northeastern University)
* Dino Oliva (Bloomberg L.P.)
* Olin Shivers (Northeastern University)

PRELIMINARY PROGRAM

Functional un|unparsing
Kenichi Asai and Oleg Kiselyov and Chung-chieh Shan

A mechanized bisimulation for the nu-calculus
Nick Benton and Vasileios Koutavas

A shallow Scheme embedding of bottom-avoiding streams
William E. Byrd and Daniel P. Friedman and Ramana Kumar and Joseph P. Near

A model of functional traversal-based generic programming
Bryan Chadwick and Karl Lieberherr

The MacScheme compiler: using denotational semantics to prove correctness
William D. Clinger

Eliminating the middle man: Learning garbage collection without interpreters
Gregory H. Cooper and Arjun Guha and Shriram Krishnamurthi

Specializing continuations
Christopher Dutchyn

A Scheme for native threads
R. Kent Dybvig

Trampolining architectures
Steven E. Ganz and Daniel P. Friedman

Finding everything that can happen: Solving authentication tests by computer
Joshua D. Guttman and John D. Ramsdell

A theory of typed hygienic macros
David Herman

The MzScheme machine and bytecode verifier
Casey L. Klein and Matthew Flatt and Robert Bruce Findler

Featherweight X10: A core calculus for async-finish parallelism
Jonathan K. Lee and Jens Palsberg

Subcubic control-flow analysis algorithms
Jan Midtgaard and David Van Horn

A simplified multi-tier semantics for Hop
Manuel Serrano and Christian Queinnec

DDP for CFA
Olin Shivers and Dimitrios Vardoulakis and Alexander Spoon

The design and implementation of Typed Scheme
Sam Tobin-Hochstadt and Matthias Felleisen

Lexical syntax thought

We reserve the single-quote character (#\') in the Scheme lexical syntax so that it can't be used anywhere in an identifier. If you stick it in the middle of an identifier (e.g., foo'bar) it lexes as three tokens ("foo", "'", "bar"). But I don't recall ever seeing anyone make use of this fact; they always stick a space before the quote.

I really miss my precious "prime" character in ML and Haskell identifiers (let val state' = munge state ...). Scheme prides itself on a permissive lexical syntax for identifiers. Why couldn't we allow quote characters in all positions of an identifier other than the first?

P.S. I know I can use the Unicode prime character (U+2032). Sorry, not till I get my Unicode keyboard.

Follow-up on effect masking and backtracking

A follow-up on yesterday's post about backtracking with state: an anonymous commenter reminded me that persistent data structures are a useful and lightweight (compared to e.g. first-class stores) approach. In fact, probably my favorite paper from ESOP 2008 was Conchon and Filliâtre's Semi-Persistent Data Structures, which was addressing exactly this problem. Rather than introducing an entirely transactional semantics for the language, it's just a data structure with a transactional interface.

Continuation marks in exceptions

Rethrowing caught exceptions is an important idiom. In particular, there are lots of cases where it's important to conditionally handle an exception by handling it and then rethrowing it. In ML, I believe it's the actual definition of pattern matching on particular exception types: the pattern matching is syntactic sugar for inspecting the caught exception and conditionally rethrowing it. In standard JavaScript it's the only way to catch particular exception types, because there is no standard conditional handling form.

But a useful feature of some exception systems, like in Java, is the association of a stack trace with an exception. But when you rethrow an exception, this involves a choice: do you want a stack trace to be associated with the original continuation that threw the exception, or the one that rethrew it? There are genuine use cases for both. But in Java, the implementers have to choose one or the other for you.

PLT Scheme gives you the flexibility to choose for yourself. Exceptions are not special values in Scheme; there's an orthogonal way of reifying the control state. The PLT runtime stores stack trace information in a special continuation mark, so if you grab the current continuation mark set, you've got your hands on a value that provides DrScheme's IDE with all the information it needs to visualize the continuation.

The standard exception types in PLT Scheme are records with a field for the current continuation mark set. So when you conditionally rethrow an exception, you can either keep its version of the continuation marks, or functionally update it with the current continuation marks and throw that instead.

Afterthought: I think Java might have chosen something like a policy where an exception value saves its stack trace at the point where it's created. This gives you the ability to do both by either rethrowing the same exception (to keep the original stack trace) or wrapping the exception with a new one (to use the new stack trace). I still prefer the PLT Scheme approach, which makes the stack trace a first-class value and consequently more explicit.

Effect masking vs. purity

I've been working for a while on an algorithm that involves two effects: mutation and backtracking. Implementation strategies for the two effects seem to have different economics. I'm working in the context of PLT Scheme, here, but I suspect my observations would be similar in other non-pure languages.

For backtracking, I could implement the algorithm in a pure way using two continuations or the list monad. Or I could just use the built-in exceptions and exception handlers of PLT Scheme. For mutation, the choice is between store-passing or the built-in mutation of Scheme.

I've tried abstracting these two effects out into a single monad for a completely pure implementation. There are downsides to this approach, though. For example, debuggers and stack traces are completely useless since most of the program control flow goes through unit, bind, and the myriad intermediate closures created by such a higher-order style of programming. Besides, an excessively higher-order style imposes real readability costs on a program. So for implementing backtracking, I find exceptions to be a more straightforward approach.

But as it turns out, the algorithm also needs to roll back mutations when it backtracks. So I simply can't use mutation. I think this is one of the things that make mutation so unwieldy--there's typically no corresponding "masking" operation for a destructive update. Exceptions have handlers, continuations (sometimes) have delimiters-- even some I/O features come with effect masks: for example, in PLT Scheme you can override the current-output-port with a string port and capture a program's output. All of these allow you to bound the effects a computation can have, to put a sort of dynamic safety net around it. Not so for set!, vector-set!, set-box!, or set-record-field!.

So for mutation, I'm sticking with explicit store-passing-- not in monadic style. That seems to be the reasonable middle ground for my purposes.

Representing failure

I'm working on an algorithm that uses backtracking implemented with exceptions and handlers (rather than, say, explicit continuations). I just noticed that, for debugging, it's nice to represent the failure exceptions as records that contain not just the data about the operation that failed but also an optional list of other failure exceptions. In the disjunction cases, I can save the intermediate failures and, if they all fail, include them in the resulting failure record. This provides me with a nice data structure representing the control flow of the failed search tree. It only required modifying about 3 lines of code and the resulting data structure is easier to analyze than a manual debugging sequence. (I hate working with debuggers, even good ones.)

Typed closure conversion

Typed closure conversion is a really lovely explanation of the structure of a closure-converted function. Every closure has its own particular environment structure that binds the particular set of free variables that occur in its body. But this means that if you represent a closure directly as a pair of an environment record and a closed procedure (which is explicitly parameterized over the environment record), then the representations of functions that are supposed to have the same type can end up with incompatible environment types. For example, the program

let val y = 1
in
  if true then
      λx.x+y
  else
      λz.z
end

converts naively to the transparent representation

let val y = 1
in
  if true then
      (λ(env, x).x+#y(env), {y=y})
  else
      (λ(env,z).z, {})
end

The problem here is the type of the environment has leaked information about the internals of the procedure into the external interface. So Minamide et al use existential types as a nice, lightweight type abstraction for hiding the environment layout as an abstract type. So you instead get the opaque representation

let val y = 1
in
  if true then
      pack {y:int} with (λ(env,x).x+#y(env), {y=y})
      as ∃t.((t × int) → int) × t
  else
      pack {} with (λ(env,z).z, {})
      as ∃t.((t × int) → int) × t
end

Update: fixed the types in the existentials-- since I'm using an uncurried representation the argument type is a pair, not an arrow type.

PLT System Facilities (Software Components): Module name resolvers

Because of eval, one program's "compile time" is another program's run-time. Even though they are not first-class, this also applies to PLT Scheme modules, since they too can be dynamically compiled, loaded and linked. As I've described before, namespaces are the general construct for managing multiple instances of modules and maintaining their top-level bindings. But I still haven't described how dynamic invocation of modules happens.

Module loading is managed by the system's module name resolver. The primary responsibility of the module name resolver is to map distinct but equivalent references to modules into canonical forms. For example, it's possible to refer to the PLT Scheme string library with either of the two forms:

(lib "string.ss" "scheme")
scheme/string

The standard module name resolver translates these to an absolute path to the module's source file in the filesystem.

The other responsibilities of the standard module name resolver are:

• to ensure that a module is only loaded once,
• to make sure each module is loaded the first time it is needed, and
• to check for and prevent cyclic loading dependencies between modules.

The module name resolver is a pretty low-level part of the PLT system. For the most part, programmers stick to using dynamic-require to interact with modules dynamically. This dynamically ensures a module is loaded and optionally selects one of its exports by name (by querying its namespace). But the module name resolver is directly accessible and can be dynamically invoked to ensure a module is loaded and resolve its name to canonical form. The module name resolver is even configurable, and can be swapped out with a custom resolver--though I have not seen this done in user code.

Matthew Flatt running for SIGPLAN member-at-large

I like Matthew's statement, so I want to call it out here:

As a SIGPLAN member at large, I would be a voice for those who believe that conferences have become too important relative to journals. Our conferences have taken over the prestige that other disciplines reserve for journals, so that our conferences tend toward more conservative acceptances and more complex reviewing processes (including double-blind submission and author-response periods), which work against the goal of broadcasting new research directions and ambitious new ideas. In comparison, our journal system, which offers the time and expertise needed for the careful review of enduring results, is left under-used and under-supported (especially by paper referees) despite the admirable efforts of journal editors. I have no easy fixes, nor do I think that immediate radical change is appropriate, but I think we should do all we can to nudge the balance back in favor of journals.

Memo to myself: directions for `svn unfail'

Sorry for this-- I keep losing this information so I'm just sticking this note to myself up here. Who knows, if other people run into this it might be of use to them, too.

If you find you're inexplicable being asked to authenticate when doing an svn up and it won't accept your password, (particularly after renaming or moving a file in the repository), here's the solution:

...if "svn up" doesn't work, you can make "svn switch" to the same url, it will update all with no problems.

Dear David Herman

Dear David Herman,

We have the same name. You seem to think you have my gmail address. Periodically I get email intended for you. It may be that you're giving out my address to people--or so I imagine, because every so often, I also get a message from Google saying that someone is initiating the process to reset my password. Naturally, I don't proceed. I don't want to reset my password. I'd prefer you stopped trying to.

I have no particular way of contacting you, because all I know is that your name is my name too, and I think you live in San Francisco (based on your mail that I've received). Which is all the more confusing, given that I spend a lot of time in the Bay Area. But I digress.

Mr. Herman, I'm afraid we can't share this gmail account. You seem to like the version without a dot, whereas I prefer the version with a dot, but either way, Google says it's mine. Sorry. I got there first.

Best regards,
David Herman

Your lambda-cube is puny.

Aaron just showed me this mind-blowing figure from a paper by van Glabbeek that attempts to abstract the wide variety of notions of equivalence in the concurrency literature:

A moment of respectful silence, please.

Hand-writing derivations

I've come to prefer one particular approach to writing out a derivation tree by hand. I used to try to draw the tree by stacking up rules with horizontal separators à la Gentzen, but I could never judge how much space I would need--I'm not accustomed to filling a page bottom to top--and one page never seemed to be enough anyway.

I've found that writing judgments top to bottom, indenting to represent nesting, is much more scalable. E.g.:

⊢ (λ f.f 1) (λ x.x) : int
  ⊢ (λ f.f 1) : (int → int) → int
    f : int → int ⊢ f 1 : int
      f : int → int ⊢ f : int → int
      f : int → int ⊢ 1 : int
  ⊢ (λ x.x) : int → int
    x : int ⊢ x : int

Make a miniature model first

I've been taught this time and time again, I've seen Cormac do it repeatedly in the ECMAScript design process, I've been told by Mitch repeatedly to do it, but it still hasn't become instinct for me: when you're facing a dauntingly large system, it's incredibly helpful to start by extracting coherent but manageably small subsets of the design and model them first. It's amazing how well that works to make a system less terrifying to work with.

PLT System Facilities (Software Components): Namespaces

So far I've described PLT Scheme's first-class component systems, as well as the second-class, static module system. Of course, Scheme is a reflective language. Where there's eval, there's not just one "compile time." Code can be compiled and evaluated at any time during the execution of a PLT Scheme virtual environment.

Moreover, considering that one of the most important applications written in PLT Scheme--DrScheme--is an IDE, it's clearly important to be able to load and reload a single module multiple times. Users have to be able to edit a module and re-evaluate it without restarting the Scheme image. (In fact, it's even possible to run DrScheme from DrScheme, so it must even be possible to have multiple instances of the same module running concurrently!)

Every instance of a module in a running PLT Scheme environment has associated with it a namespace. Namespaces serve two somewhat orthogonal purposes. The first is to store top-level bindings. A module's namespace contains the mapping of its global definitions (some of which may be made available to other modules via provide). There is also a namespace associated with the REPL, which can be dynamically modified; in DrScheme, that namespace is typically just the one associated with the current running instance of the module being edited. In a sense, this role of namespaces is to mediate between the static, segmented architecture of modules and the dynamic, global nature of the Scheme top-level. This is an interesting tension that comes in whenever designing a lexically scoped language with dynamic code evaluation such as with eval or a REPL.

The second purpose of namespaces is to maintain an internal module registry, which keeps track of running instances of modules. Every namespace has its own registry, but registries may share instances. This is how it's possible both to create multiple, isolated instances of modules and to share module instances and their associated state.

Cognitive dissonance and correctness

I don't pretend to be a psychologist, but I find the mental process of getting a program correct fascinating. It feels like the process goes something like this:

1. Cognitive dissonance ("this can't possibly always work, can it?")
2. Confronting the danger ("what might go wrong?")
3. Questioning assumptions ("what am I assuming, and why do I need to assume it?")
4. Codifying assumptions as invariants ("P")
5. Pushing invariants through the program ("∀x. P(x)")

There are lots of techniques for #5, of course, and modularity helps make it manageable; e.g., defensively add in checks to enforce P so it's safe to assume.

But the interesting part to me is really the fact that, if you have the discipline to follow it through, it's precisely that queasy feeling that something might go wrong that eventually leads you to discover the program's invariants and ultimately to get the program right.

I mentioned this to Mitch, and he added "it's that recognition of danger (#1) that keeps us honest."

's Birthday is Coming Up...

I wonder if early in life, 's parents used to call him/her little baby epsilon.

Whoa

This is a really neat new feature of the Northeastern University library catalog:

Unless you spend the next 10 minutes taking screen shots and blogging about it, this is really convenient. And it saves our precious reserves of little scraps of paper.

PLT System Facilities (Software Components): Modules

Lexical scope in general and lambda in particular go a long way towards supporting modular, separate development. As I mentioned before, PLT Scheme builds a number of first-class, module-like component systems on top of lambda. But it also contains a more primitive module system in which modules are not first-class. This serves a number of purposes.

First of all, static modules provide systematic support for packaging, compiling, and deploying code. First-class modules are flexible and expressive, but they don't have anything to say about compilation and deployment. Somewhere along the line there has to be a notion of what the compiler takes as input, and when you have separate development, you need separate deployment and ideally separate compilation.

Another critical purpose of static modules is the ability to modularize static entities in a language. In ML, for example, modules can import and export types. Scheme is of course more [ed: dynamic] than ML, but it still has its own crucial compile-time abstractions: macros. With dynamic modules, there's no straightforward way to import and export static entities like macros. A secondary benefit of static modules is that you can import all the bindings from another module at once without having to spell them all out; this is admittedly less important but still very convenient.

Finally, PLT Scheme was designed to support multiple languages. For pedagogical purposes, this has allowed them to design multiple, concentric subsets of the language tailored to the How to Design Programs curriculum. This has also facilitated language research by making it easy to design and implement new languages (by macro-compiling them to Scheme) and to research language interactions in a multi-language environment. The relevant piece of the module system is a single hook at the beginning of a module definition: the grammar of a module is an S-expression containing the symbol module, a symbol naming the module, and an S-expression indicating the language of the body:

(module foo scheme body ...)

Typically the language chosen is the special built-in language scheme, as above, or the somewhat leaner scheme/base. But the language position works by simply importing another module that implements the required macros for compiling the body. In place of scheme, you can put in a module path for any module installed on the system.

It's also possible to specify a custom reader for a PLT language so it doesn't even have to be restricted to an S-expression syntax. The initial reader allows you to specify a language with the special shebang-like #lang syntax:

#lang scheme/base
body ...

From that point on, the language's reader has access to the input stream to parse it any way it likes.

Anyone can implement a language module, which means people have developed PLT implementations of Algol, Java, ML, and JavaScript, to name a few.

Update: Added in the missing word "dynamic" above. Also, this is a better link for module paths.

Also, Sam is right in the comments: the scheme language really isn't special or built-in in any significant way. It's simply another module provided in the standard PLT collections.

Ooh, that's pretty

OS X calculator "programmer" view:

PLT System Facilities (Software Components): Lexical scope

Like any programming system, PLT Scheme involves multiple people and a lot of code. So managing software components is a primary concern. And of course, as a Scheme, PLT uses lexical scope as the linguistic linchpin for managing software. The importance of lexical scope in a component architecture is that it allows code to be shared and mixed while guaranteeing the internal integrity of components.

With the power of macros, PLT has developed a number of software component abstractions on top of little lambda. One of these is a single-inheritance, class- and interface-based OOP system. Classes are first-class values, which means it's easy to implement mixins (i.e., classes parameterized over their superclass) as functions that return classes. More recently, they've introduced traits, which are like fragments of classes that can be more freely and flexibly combined than mixins. Also built with macros is the unit system, which is a first-class, parameterized, recursive module system.

All of these abstractions admit modular and separate development because they protect the internal integrity of their local bindings and definitions. You can hand out a component into an untrusted context and know that it won't be able to modify or even inspect the component's internals. And you can reason locally about your code knowing that no context can change its behavior based on these internals.

The PLT Scheme Operating System

Back in the day, programming languages were considered a systems concern. These days a lot of PL research is done in a vacuum, with abstract models and stand-alone prototypes. But programming languages rise and fall by their applications, and the deployment of a language always involves interesting and non-trivial systems challenges.

The PLT group has done a ton of work in this area. A decade ago, Matthew, Robby, Shriram and Matthias wrote an ICFP paper on Programming Languages as Operating Systems, sketching a few of the highlights of the PLT virtual machine. They focused on MrEd, the GUI engine. But taking a step back, there are many more systems-y facilities in PLT Scheme than just the UI infrastructure. And of course, that paper is a decade old and beginning to show its age.

I'm planning to write a series of posts on some of the myriad systems facilities in PLT Scheme and how they fit together.

I feel much better about myself

I'd always felt stupid for being stymied by the syntax of C declarations. But I think I get it now.

First of all, you have to understand that a C declaration starts with one single base type followed by a sequence of fragments of declarations; you essentially can interpret this as a sequence of separate declarations, each created by plugging the base type into each separate fragment. Syntactically, the "hole" inside each fragment actually contains the name of the identifier being bound; conceptually, you pull out that identifier and bind it to the type you get by plugging the base type into the position where you found the identifier.

For example:

int x, *y, z[3];

declares an int x, an int pointer y, and an int array z. Now for function types, the base type is interpreted as the return type; in other words, a fragment of a declaration of function type has its "hole" in the return type position. So:

int x, f(char);

declares an integer x and a function f of type char → int. Next we have to worry about pointer types. Oh, pointer types. First of all, you have to know that pointer types in the declaration are associated with the fragments, not the base type. So:

int *p, x;

declares an int pointer p and a plain int x. Now, notice that the asterisk is a prefix operator, whereas the function and array type constructors are postfix operators. So now we get to worry about precedence. You just have to remember that the asterisk binds loosest. So:

int *f(char);

is a function that returns an int pointer, whereas

int (*f)(char);

is a pointer to a function that returns an int. (You can throw in parentheses most anywhere in these things; forgot to mention that.) Okay, but here's the kicker: the nesting of type constructors is interpreted inside-out. Consider:

int (*(foo[3]))(char);

((Not that it helps, but I've over-parenthesized to avoid precedence issues.)) If you're still trying, you might be tempted to read this as declaring a function that returns an array of int pointers, or maybe a pointer to an array of ints. But the inner-most syntactically nested type constructor is interpreted as the outer-most semantically nested type constructor. So foo is in fact an array of pointers to functions.

My first PLT patch

I've submitted my first patch to the internals of PLT Scheme. It's a tiny thing: the ability to unquote inside a quasiquoted hash-table literal, e.g.:

> `#hash((x . ,(+ 1 2)))
#hash((x . 3))

And Matthew had to fix up some issues with it.

But anyway, making contributions to PLT is easier these days due to a couple of factors. First, the creation of plt-dev, a public mailing list for discussing the development of PLT Scheme, means that there's better support for people who want to contribute. Second, I'm told that more of the internals of PLT Scheme are self-hosted than apparently they used to be, i.e. a lot of PLT Scheme is itself implemented in PLT Scheme. This makes it a lot less scary to dive into the code.

The C Typedef Parsing Problem

The well-known "typedef problem" with parsing C is that the standard C grammar is ambiguous unless the lexer distinguishes identifiers bound by typedef and other identifiers as two separate lexical classes. This means that the parser needs to feed scope information to the lexer during parsing. One upshot is that lexing must be done concurrently with parsing. That's standard, although because parser generators usually allow fixed lookahead, you have to pay very close attention to making sure the lexer stays properly in synch with the parser, even when it gets ahead. For example:

typedef int my_int;
my_int x;

At the semicolon, the type environment needs to be updated with an entry for my_int. But if the lexer has already looked ahead to my_int, it will have lexed it as an identifier rather than a type name. But this is just a small matter of heroic hacking.

The real problem is a larger engineering one. Just to parse a program, you need to have the full type environment. And the program you're parsing may have included other programs. So if you want to write tools that perform analyses on fragments of C, you still have to feed them the entire environment one way or another. Either that becomes a requirement you foist onto the user ("this tool takes two inputs: a fragment of C and an initial type environment"), or you only allow whole programs instead of fragments, or you use an ambiguous grammar with, say, a GLR parser and divine some clever disambiguation heuristics.

And of course, C's braindead non-module-system is just a preprocessor directive (#include). So if you punt and require whole programs, that means you have to implement the C preprocessor, too. Or at least feed it through an existing implementation of the C preprocessor. And then process stdio.h, stdlib.h, etc. etc. every time you analyze just about any C program. So then you start thinking about caching results of #include for efficiency...

All this because of one silly grammar ambiguity.

History lesson

A history and semantics lesson from Matthias on plt-scheme:

Normal order and applicative order are failed attempts to explain the nature of call-by-name programming languages and call-by-value programming languages as models of the lambda calculus. Each describes a so-called reduction strategy, which is an algorithm that picks the position of next redex BETA that should be reduced. By 1972, it was clear that instead you want different kind of calculi for different calling conventions and evaluation strategies (to the first outermost lambda, not inside). That is, you always reduce at the leftmost-outermost point in a program but you use either BETA-NAME or BETA-VALUE. Non-PL people were confused (and still are) because BETA-NAME looks like BETA but nearly 40 years later, everyone should figure this out. SICP was written when the majority of people were still confused. -- Matthias

A funny reader context

Trivia time: find a place in the Scheme reader where ,expr is not equivalent to (unquote expr).

Answer:

> (define ls '(1 2 3))
> `#(unquote ls)
#(1 2 3)
> `#,ls
#,ls

Using C to talk to C

I've released the first version of a PLaneT package for working with C. It's based on an idea I got from Felix Klock's Scheme Workshop 2008 paper: rather than try to do manual pointer arithmetic based on the current architecture's ABI, you can find out byte offsets of data structures by creating a C program that tells you what they should be. So that's what c.plt allows you to do; using a system-installed C compiler, you can generate a representation of the binary layouts of data structures. Here's a sample interaction:

> (define time.h
   (make-header
     #reader (planet dherman/c/reader) {
         struct tm {
             int tm_sec;
             int tm_min;
             int tm_hour;
             int tm_mday;
             int tm_mon;
             int tm_year;
             int tm_wday;
             int tm_yday;
             int tm_isdst;
         };
     }))
> (define time-abi
   (compile-header time.h
     (system-compiler #:include<> '("time.h") gcc)))
> (layout-size (time-abi 'tm))
36
> (layout-offset (time-abi 'tm) 'tm_sec)
0
> (layout-offset (time-abi 'tm) 'tm_year)
20

Quiz answer

Reader Mitch (not my advisor, apparently) comes closest to the answer to my quiz question:

Some kind of alignment thing? I can't think of how code would be affected by that, though.

As it happens, changing the code was affecting the particular size of the activation record allocated by the GCC-generated code. Somehow the extra code ended up with a slightly smaller activation record. And then it turned out that the slight difference (something like 8 or 16 bytes) was pushing the activation record over the edge of a page boundary. Boom!

It's still a mystery to me exactly how throwing in an asm("noop\n") can affect the size of the activation record. Such are the arcane mysteries of GCC code generation. I had to catch my flight home before Dave had worked out all the details but by now I bet he has an even better understanding of it. It was fun and inspiring to watch Dave's detective skills in action.

Quiz question

Here's a fun puzzle I watched Dave Mandelin track down yesterday. Why would adding a guaranteed no-op such as

if (FALSE) { printf("can't happen\n"); }

or even

asm("noop\n");

to the body of a procedure cause a program to run measurably and consistently faster? I'll post the answer later today. (Or as much as I understand, anyway.)

Java, we don't care about you

Joel Spolsky pretty much nails it.

I actually grabbed a screen shot of this very same dialog box some time last year because it was so absurd. The part that always amazes me is why people think customers are going to care about their product as much as they do. It seems to me that I'm more likely to be loyal to a technology brand that shows a little humility and restraint.

A page of the dissertation

Ron Garcia suggested that I should get in the practice of writing a little bit for my dissertation each day, so that when crunch time comes, I'll already have a lot of material to work with. This being New Year's, I should also go to the gym, eat healthier, clean my home and my office, make a budget, fix more bugs, and organize my time.

But I just wrote my first page of content for the dissertation, and that feels pretty good. There's even a lemma!

Fexprs? in Scheme?

“The top level is hopeless.”
     -- Matthew Flatt [1] [2] [3] [4] [5] [6] [7] [8] [9]

Scheme's top level allows for interactive evaluation such as at the REPL, where global definitions can be dynamically evaluated one by one. To allow for forward references, free variables are not a static error at the top level. But global definitions may be macros, and there's no way to know whether a forward reference is eventually going to turn out to be a value binding or a macro binding. So one simple semantics is just to assume that forward references are always value bindings and compile them as such. But then you get unsatisfying interactions like this:

> (define (f) (display (g 42)))
> (define-syntax g (syntax-rules () ((g x) (quote x))))
> (f)

reference to an identifier before its definition: g

It's worse with macro-defining macros. For example, a define/inline form would bind its definition as a macro, but the user could generally treat it as a value binding. But you'd still run into the same problem:

> (define/inline (f) (g 42))
> (define/inline (g n) (add1 n))
> (f)

reference to an identifier before its definition: g

What's in conflict in Scheme is the desire for macros to be a static, compile-time entity and the REPL to allow dynamic, incremental update to the global environment. In fact, the top level seems to be the one place in Scheme where programmers expect behavior something like Lisp's antiquated fexprs. Bear with me...

Imagine if the compiler treated any form (x . s) where x is a top-level variable reference--bound or unbound--as an uninterpreted syntax object waiting to be parsed. Then only when the form is evaluated would x be looked up in the global environment to determine how to compile the form. If x is unbound, it's a dynamic error; if it's a value, it's compiled and evaluated as a function application; if it's a macro, it's macro-expanded, compiled, and evaluated. This would accomodate any sequence of definitions and redefinitions of top-level bindings, either as value bindings, macro bindings, or both. For example:

> (define (foo x) (f x))
> (define (f x) (add1 x))
> (foo 41)
42
> (define-syntax f (syntax-rules () ((f e) (quote e))))
> (foo 41)
x

This has a lot of the similarities to fexprs; it means a function like foo is subject to dynamic reparsing: at one point it calls a function on x and at another point it applies a macro. But whereas with fexprs, any application expression may be dynamically reparsed, here this would only be the case for applications of top-level variables.

Fexprs are bad for two reasons: they make the language hard to compile efficiently and they make programs hard to understand by subjecting the basic program definition to dynamic reinterpretation. To be sure, making Scheme's top-level fexpr-like would make efficient compilation harder. But the top-level is the part of Scheme where programs are dynamically defined. Users are constantly surprised at the behavior of top-level forward references and macro definitions. What they seem to naturally expect is, in some sense, fexprs.