Wednesday, July 22, 2009

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.

Monday, July 13, 2009

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.

Sunday, July 12, 2009

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.

Thursday, July 09, 2009

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